let U1, U2 be Universal_Algebra; 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; ( h is_monomorphism U1,U2 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 13;
then A1:
dom (MSAlg h) = {0 }
by PARTFUN1:def 4;
assume A2:
h is_monomorphism U1,U2
; MSAlg h is_monomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1)
then A3:
h is_homomorphism U1,U2
by ALG_1:def 2;
hence
MSAlg h is_homomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1)
by Th16; MSUALG_3:def 11 MSAlg h is "1-1"
U1,U2 are_similar
by A3, ALG_1:def 1;
then
MSAlg h = 0 .--> h
by Def3, Th10;
then A4:
(MSAlg h) . 0 = h
by FUNCOP_1:87;
let i be set ; MSUALG_3:def 2 for b1 being set holds
( not i in proj1 (MSAlg h) or not (MSAlg h) . i = b1 or b1 is one-to-one )
let h9 be Function; ( not i in proj1 (MSAlg h) or not (MSAlg h) . i = h9 or h9 is one-to-one )
assume
( i in dom (MSAlg h) & (MSAlg h) . i = h9 )
; h9 is one-to-one
then
h = h9
by A4, A1, TARSKI:def 1;
hence
h9 is one-to-one
by A2, ALG_1:def 2; verum
reconsider g = (*--> 0 ) * (signature U1) as Function of (dom (signature U1)),({0 } * ) by MSUALG_1:7;