let U1, U2 be Universal_Algebra; :: thesis: ( U1,U2 are_similar implies Inv the carrier of U1,the carrier of U2 is Function of the carrier of [:U1,U2:],the carrier of [:U2,U1:] )
assume U1,U2 are_similar ; :: thesis: Inv the carrier of U1,the carrier of U2 is Function of the carrier of [:U1,U2:],the carrier of [:U2,U1:]
then ( [:U1,U2:] = UAStr(# [:the carrier of U1,the carrier of U2:],(Opers U1,U2) #) & [:U2,U1:] = UAStr(# [:the carrier of U2,the carrier of U1:],(Opers U2,U1) #) ) by Def5;
hence Inv the carrier of U1,the carrier of U2 is Function of the carrier of [:U1,U2:],the carrier of [:U2,U1:] ; :: thesis: verum