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

( 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

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

then A7:
G ** F is "onto"
;
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;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

( 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