let U1, U2 be Universal_Algebra; :: thesis: for h being Function of U1,U2 st h is_monomorphism holds
MSAlg h is_monomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1)
let h be Function of U1,U2; :: thesis: ( h is_monomorphism implies MSAlg h is_monomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) )
set f = MSAlg h;
the carrier of (MSSign U1) = {0} by MSUALG_1:def 8;
then A1: dom (MSAlg h) = {0} by PARTFUN1:def 2;
assume A2: h is_monomorphism ; :: thesis: MSAlg h is_monomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1)
then A3: h is_homomorphism ;
hence MSAlg h is_homomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) by Th16; :: according to MSUALG_3:def 9 :: thesis: MSAlg h is "1-1"
U1,U2 are_similar by A3;
then MSAlg h = 0 .--> h by Def3, Th10;
then A4: (MSAlg h) . 0 = h by FUNCOP_1:72;
let i be set ; :: according to MSUALG_3:def 2 :: thesis: for b₁ being set holds
( not i in dom (MSAlg h) or not (MSAlg h) . i = b₁ or b₁ is one-to-one )
let h9 be Function; :: thesis: ( not i in dom (MSAlg h) or not (MSAlg h) . i = h9 or h9 is one-to-one )
assume ( i in dom (MSAlg h) & (MSAlg h) . i = h9 ) ; :: thesis: h9 is one-to-one
then h = h9 by A4, A1, TARSKI:def 1;
hence h9 is one-to-one by A2; :: thesis: verum