let U1, U2 be Universal_Algebra; :: thesis: for h being Function of U1,U2 st h is_isomorphism U1,U2 holds
MSAlg h is_isomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1)
let h be Function of U1,U2; :: thesis: ( h is_isomorphism U1,U2 implies MSAlg h is_isomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) )
set A = (MSAlg U2) Over (MSSign U1);
set f = MSAlg h;
assume A1: h is_isomorphism U1,U2 ; :: thesis: MSAlg h is_isomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1)
then h is_epimorphism U1,U2 by ALG_1:def 4;
hence MSAlg h is_epimorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) by Th18; :: according to MSUALG_3:def 12 :: thesis: MSAlg h is_monomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1)
h is_monomorphism U1,U2 by A1, ALG_1:def 4;
hence MSAlg h is_monomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) by Th19; :: thesis: verum