let U1, U2 be Universal_Algebra; :: thesis: for h being Function of U1,U2 st h is_monomorphism U1,U2 holds
MSAlg h is_monomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1)
let h be Function of U1,U2; :: thesis: ( h is_monomorphism U1,U2 implies MSAlg h is_monomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) )
assume A1: h is_monomorphism U1,U2 ; :: thesis: MSAlg h is_monomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1)
set f = MSAlg h;
A2: h is_homomorphism U1,U2 by A1, ALG_1:def 2;
then A3: U1,U2 are_similar by ALG_1:def 1;
thus MSAlg h is_homomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) by A2, Th16; :: according to MSUALG_3:def 11 :: thesis: MSAlg h is "1-1"
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 h' be Function; :: thesis: ( not i in dom (MSAlg h) or not (MSAlg h) . i = h' or h' is one-to-one )
assume that
A4: i in dom (MSAlg h) and
A5: (MSAlg h) . i = h' ; :: thesis: h' is one-to-one
reconsider g = (*--> 0 ) * (signature U1) as Function of dom (signature U1),{0 } * by MSUALG_1:7;
A6: ( the carrier of (MSSign U1) = {0 } & the carrier' of (MSSign U1) = dom (signature U1) & the Arity of (MSSign U1) = g & the ResultSort of (MSSign U1) = (dom (signature U1)) --> 0 ) by MSUALG_1:def 13;
MSAlg h = 0 .--> h by A3, Def3, Th10;
then A7: (MSAlg h) . 0 = h by FUNCOP_1:87;
dom (MSAlg h) = {0 } by A6, PBOOLE:def 3;
then h = h' by A4, A5, A7, TARSKI:def 1;
hence h' is one-to-one by A1, ALG_1:def 2; :: thesis: verum