let U1, U2 be Universal_Algebra; :: thesis: for h being Function of U1,U2 st h is_epimorphism holds
MSAlg h is_epimorphism MSAlg U1,(MSAlg U2) Over (MSSign U1)
let h be Function of U1,U2; :: thesis: ( h is_epimorphism implies MSAlg h is_epimorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) )
set f = MSAlg h;
set A = (MSAlg U2) Over (MSSign U1);
A1: 0 in {0} by TARSKI:def 1;
MSSorts U2 = 0 .--> the carrier of U2 by MSUALG_1:def 9;
then A2: ( the carrier of (MSSign U1) = {0} & (MSSorts U2) . 0 = the carrier of U2 ) by A1, FUNCOP_1:7, MSUALG_1:def 8;
A3: MSAlg U2 = MSAlgebra(# (MSSorts U2),(MSCharact U2) #) by MSUALG_1:def 11;
assume A4: h is_epimorphism ; :: thesis: MSAlg h is_epimorphism MSAlg U1,(MSAlg U2) Over (MSSign U1)
then A5: rng h = the carrier of U2 ;
A6: h is_homomorphism by A4;
then A7: U1,U2 are_similar ;
then MSSign U1 = MSSign U2 by Th10;
then A8: the Sorts of ((MSAlg U2) Over (MSSign U1)) = MSSorts U2 by A3, Th9;
thus MSAlg h is_homomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) by A6, Th16; :: according to MSUALG_3:def 8 :: thesis: MSAlg h is "onto"
let i be set ; :: according to MSUALG_3:def 3 :: thesis: ( not i in the carrier of (MSSign U1) or rng ((MSAlg h) . i) = the Sorts of ((MSAlg U2) Over (MSSign U1)) . i )
assume i in the carrier of (MSSign U1) ; :: thesis: rng ((MSAlg h) . i) = the Sorts of ((MSAlg U2) Over (MSSign U1)) . i
then reconsider i9 = i as Element of (MSSign U1) ;
reconsider h9 = (MSAlg h) . i as Function of ( the Sorts of (MSAlg U1) . i9),( the Sorts of ((MSAlg U2) Over (MSSign U1)) . i9) by PBOOLE:def 15;
(MSAlg h) . 0 = (0 .--> h) . 0 by A7, Def3, Th10
.= h by A1, FUNCOP_1:7 ;
then ( the carrier of (MSSign U1) = {0} & rng h9 = the Sorts of ((MSAlg U2) Over (MSSign U1)) . 0 ) by A5, A8, A2, TARSKI:def 1;
hence rng ((MSAlg h) . i) = the Sorts of ((MSAlg U2) Over (MSSign U1)) . i by TARSKI:def 1; :: thesis: verum