let A, B be strict SubAlgebra of U2; :: thesis: ( the carrier of A = f .: the carrier of U1 & the carrier of B = f .: the carrier of U1 implies A = B )
assume A21: ( the carrier of A = f .: the carrier of U1 & the carrier of B = f .: the carrier of U1 ) ; :: thesis: A = B
reconsider A1 = the carrier of A, B1 = the carrier of B as non empty Subset of U2 by UNIALG_2:def 8;
( the charact of A = Opers U2,A1 & the charact of B = Opers U2,B1 ) by UNIALG_2:def 8;
hence A = B by A21; :: thesis: verum