let U1, U2 be Universal_Algebra; :: thesis: for h being Function of U1,U2 st U1,U2 are_similar & MSAlg h is_isomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) holds
h is_isomorphism U1,U2
let h be Function of U1,U2; :: thesis: ( U1,U2 are_similar & MSAlg h is_isomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) implies h is_isomorphism U1,U2 )
assume A1: U1,U2 are_similar ; :: thesis: ( not MSAlg h is_isomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) or h is_isomorphism U1,U2 )
assume A2: MSAlg h is_isomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) ; :: thesis: h is_isomorphism U1,U2
then MSAlg h is_monomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) by MSUALG_3:def 12;
hence h is_monomorphism U1,U2 by A1, Th23; :: according to ALG_1:def 4 :: thesis: h is_epimorphism U1,U2
MSAlg h is_epimorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) by A2, MSUALG_3:def 12;
hence h is_epimorphism U1,U2 by A1, Th22; :: thesis: verum