let U1, U2 be Universal_Algebra; :: thesis: for h being Function of U1,U2 st U1,U2 are_similar & MSAlg h is_epimorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) holds
h is_epimorphism U1,U2
let h be Function of U1,U2; :: thesis: ( U1,U2 are_similar & MSAlg h is_epimorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) implies h is_epimorphism U1,U2 )
assume A1:
U1,U2 are_similar
; :: thesis: ( not MSAlg h is_epimorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) or h is_epimorphism U1,U2 )
assume A2:
MSAlg h is_epimorphism MSAlg U1,(MSAlg U2) Over (MSSign U1)
; :: thesis: h is_epimorphism U1,U2
then A3:
MSAlg h is_homomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1)
by MSUALG_3:def 10;
A4:
MSSign U1 = MSSign U2
by A1, Th10;
A5:
MSAlg h is "onto"
by A2, MSUALG_3:def 10;
set B = the Sorts of ((MSAlg U2) Over (MSSign U1));
set I = the carrier of (MSSign U1);
A6:
the carrier of (MSSign U1) = {0 }
by MSUALG_1:def 13;
A7:
0 in {0 }
by TARSKI:def 1;
A8: (MSAlg h) . 0 =
(0 .--> h) . 0
by A1, Def3, Th10
.=
h
by A7, FUNCOP_1:13
;
MSSorts U2 = 0 .--> the carrier of U2
by MSUALG_1:def 14;
then A9:
(MSSorts U2) . 0 = the carrier of U2
by A7, FUNCOP_1:13;
A10:
the Sorts of ((MSAlg U2) Over (MSSign U1)) = the Sorts of (MSAlg U2)
by A4, Th9;
A11:
MSAlg U2 = MSAlgebra(# (MSSorts U2),(MSCharact U2) #)
by MSUALG_1:def 16;
thus
h is_epimorphism U1,U2
:: thesis: verumproof
thus
h is_homomorphism U1,
U2
by A1, A3, Th21;
:: according to ALG_1:def 3 :: thesis: rng h = the carrier of U2
thus
rng h = the
carrier of
U2
by A5, A6, A7, A8, A9, A10, A11, MSUALG_3:def 3;
:: thesis: verum
end;