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 ;
f is_monomorphism by A1;
then A2: f is one-to-one ;
then A3: rng (f ") = dom f by FUNCT_1:33
.= the carrier of U1 by FUNCT_2:def 1 ;
A4: f is_epimorphism by A1;
dom (f ") = rng f by A2, FUNCT_1:33
.= the carrier of U2 by A4 ;
then reconsider g = f " as Function of U2,U1 by A3, FUNCT_2:def 1, RELSET_1:4;
take g ; :: according to ALG_1:def 5 :: thesis: g is_isomorphism
thus g is_isomorphism by A1, Th10; :: thesis: verum