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 )
reconsider A1 = the carrier of A, B1 = the carrier of B as non empty Subset of U2 by UNIALG_2:def 8;
A26: the charact of A = Opers U2,A1 by UNIALG_2:def 8;
assume ( the carrier of A = f .: the carrier of U1 & the carrier of B = f .: the carrier of U1 ) ; :: thesis: A = B
hence A = B by A26, UNIALG_2:def 8; :: thesis: verum