let U1, U2 be Universal_Algebra; :: thesis: ( U1,U2 are_isomorphic implies U2,U1 are_isomorphic )
assume U1,U2 are_isomorphic ; :: thesis: U2,U1 are_isomorphic
then consider f being Function of U1,U2 such that
A1: f is_isomorphism U1,U2 by Def5;
f is_monomorphism U1,U2 by A1, Def4;
then A2: f is one-to-one by Def2;
then A3: rng (f " ) = dom f by FUNCT_1:55
.= the carrier of U1 by FUNCT_2:def 1 ;
A4: f is_epimorphism U1,U2 by A1, Def4;
dom (f " ) = rng f by A2, FUNCT_1:55
.= the carrier of U2 by A4, Def3 ;
then reconsider g = f " as Function of U2,U1 by A3, FUNCT_2:def 1, RELSET_1:11;
take g ; :: according to ALG_1:def 5 :: thesis: g is_isomorphism U2,U1
thus g is_isomorphism U2,U1 by A1, Th11; :: thesis: verum