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