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
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 )
set B = the Sorts of ((MSAlg U2) Over (MSSign U1));
set I = the carrier of (MSSign U1);
A1: 0 in {0} by TARSKI:def 1;
MSSorts U2 = 0 .--> the carrier of U2 by MSUALG_1:def 9;
then A2: (MSSorts U2) . 0 = the carrier of U2 by A1, FUNCOP_1:7;
A3: ( the carrier of (MSSign U1) = {0} & MSAlg U2 = MSAlgebra(# (MSSorts U2),(MSCharact U2) #) ) by MSUALG_1:def 8, MSUALG_1:def 11;
assume A4: U1,U2 are_similar ; :: thesis: ( not MSAlg h is_epimorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) or h is_epimorphism )
then MSSign U1 = MSSign U2 by Th10;
then A5: the Sorts of ((MSAlg U2) Over (MSSign U1)) = the Sorts of (MSAlg U2) by Th9;
assume A6: MSAlg h is_epimorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) ; :: thesis: h is_epimorphism
then A7: MSAlg h is "onto" ;
MSAlg h is_homomorphism MSAlg U1,(MSAlg U2) Over (MSSign U1) by A6;
then A8: h is_homomorphism by A4, Th21;
(MSAlg h) . 0 = (0 .--> h) . 0 by A4, Def3, Th10
.= h by A1, FUNCOP_1:7 ;
then rng h = the carrier of U2 by A7, A1, A2, A5, A3;
hence h is_epimorphism by A8; :: thesis: verum