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