let U1, U2 be Universal_Algebra; :: thesis: for h being Function of U1,U2 st U1,U2 are_similar & MSAlg h is_monomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) holds
h is_monomorphism
let h be Function of U1,U2; :: thesis: ( U1,U2 are_similar & MSAlg h is_monomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) implies h is_monomorphism )
assume A1: U1,U2 are_similar ; :: thesis: ( not MSAlg h is_monomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) or h is_monomorphism )
assume A2: MSAlg h is_monomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) ; :: thesis: h is_monomorphism
then A3: MSAlg h is "1-1" ;
MSAlg h is_homomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) by A2;
then A4: h is_homomorphism by A1, Th21;
A5: the carrier of (MSSign U1) = {0} by MSUALG_1:def 8;
A6: 0 in {0} by TARSKI:def 1;
(MSAlg h) . 0 = (0 .--> h) . 0 by A1, Def3, Th10
.= h by A6, FUNCOP_1:7 ;
then h is one-to-one by A3, A5, A6, MSUALG_3:1;
hence h is_monomorphism by A4; :: thesis: verum