-lemma lsubf_inv_unit_sn: â\88\80g1,f2,I,J,K1,K2,V. â¦\83K1.â\93\91{I}V, ⫯g1⦄ ⫃𝐅* ⦃K2.ⓤ{J}, f2⦄ →
- â\88\83â\88\83g,g0,g2. â¦\83K1, g0â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & K1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 g & g0 â\8b\93 g â\89\98 g1 & f2 = ⫯g2.
+lemma lsubf_inv_unit_sn: â\88\80g1,f2,I,J,K1,K2,V. â¦\83K1.â\93\91{I}V, â\86\91g1⦄ ⫃𝐅* ⦃K2.ⓤ{J}, f2⦄ →
+ â\88\83â\88\83g,g0,g2. â¦\83K1, g0â¦\84 â«\83ð\9d\90\85* â¦\83K2, g2â¦\84 & K1 â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 g & g0 â\8b\93 g â\89\98 g1 & f2 = â\86\91g2.