let S be non empty non void ManySortedSign ; :: thesis: for U1, U2, U3 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U2,U3 st F is_epimorphism U1,U2 & G is_epimorphism U2,U3 holds
G ** F is_epimorphism U1,U3
let U1, U2, U3 be non-empty MSAlgebra over S; :: thesis: for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U2,U3 st F is_epimorphism U1,U2 & G is_epimorphism U2,U3 holds
G ** F is_epimorphism U1,U3
let F be ManySortedFunction of U1,U2; :: thesis: for G being ManySortedFunction of U2,U3 st F is_epimorphism U1,U2 & G is_epimorphism U2,U3 holds
G ** F is_epimorphism U1,U3
let G be ManySortedFunction of U2,U3; :: thesis: ( F is_epimorphism U1,U2 & G is_epimorphism U2,U3 implies G ** F is_epimorphism U1,U3 )
assume that
A1: F is_epimorphism U1,U2 and
A2: G is_epimorphism U2,U3 ; :: thesis: G ** F is_epimorphism U1,U3
A3: G is "onto" by A2;
A4: F is "onto" by A1;
for i being set st i in the carrier of S holds
rng ((G ** F) . i) = the Sorts of U3 . i
proof
let i be set ; :: thesis: ( i in the carrier of S implies rng ((G ** F) . i) = the Sorts of U3 . i )
assume A5: i in the carrier of S ; :: thesis: rng ((G ** F) . i) = the Sorts of U3 . i
then reconsider f = F . i as Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) by PBOOLE:def 15;
reconsider g = G . i as Function of ( the Sorts of U2 . i),( the Sorts of U3 . i) by A5, PBOOLE:def 15;
rng f = the Sorts of U2 . i by A4, A5;
then A6: dom g = rng f by A5, FUNCT_2:def 1;
rng g = the Sorts of U3 . i by A3, A5;
then rng (g * f) = the Sorts of U3 . i by A6, RELAT_1:28;
hence rng ((G ** F) . i) = the Sorts of U3 . i by A5, Th2; :: thesis: verum
end;
then A7: G ** F is "onto" ;
( F is_homomorphism U1,U2 & G is_homomorphism U2,U3 ) by A1, A2;
then G ** F is_homomorphism U1,U3 by Th10;
hence G ** F is_epimorphism U1,U3 by A7; :: thesis: verum