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_monomorphism U1,U2 & G is_monomorphism U2,U3 holds
G ** F is_monomorphism 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_monomorphism U1,U2 & G is_monomorphism U2,U3 holds
G ** F is_monomorphism U1,U3
let F be ManySortedFunction of U1,U2; :: thesis: for G being ManySortedFunction of U2,U3 st F is_monomorphism U1,U2 & G is_monomorphism U2,U3 holds
G ** F is_monomorphism U1,U3
let G be ManySortedFunction of U2,U3; :: thesis: ( F is_monomorphism U1,U2 & G is_monomorphism U2,U3 implies G ** F is_monomorphism U1,U3 )
assume that
A1: F is_monomorphism U1,U2 and
A2: G is_monomorphism U2,U3 ; :: thesis: G ** F is_monomorphism U1,U3
A3: G is "1-1" by A2;
A4: F is "1-1" by A1;
for i being set
for h being Function st i in dom (G ** F) & (G ** F) . i = h holds
h is one-to-one

proof

let i be set ; :: thesis: for h being Function st i in dom (G ** F) & (G ** F) . i = h holds
h is one-to-one
let h be Function; :: thesis: ( i in dom (G ** F) & (G ** F) . i = h implies h is one-to-one )
assume that
A5: i in dom (G ** F) and
A6: (G ** F) . i = h ; :: thesis: h is one-to-one
A7: i in the carrier of S by A5, PARTFUN1:def 2;
then reconsider g = G . i as Function of ( the Sorts of U2 . i),( the Sorts of U3 . i) by PBOOLE:def 15;
reconsider f = F . i as Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) by A7, PBOOLE:def 15;
i in dom G by A7, PARTFUN1:def 2;
then A8: g is one-to-one by A3;
i in dom F by A7, PARTFUN1:def 2;
then f is one-to-one by A4;
then g * f is one-to-one by A8;
hence h is one-to-one by A6, A7, Th2; :: thesis: verum

end;

then A9: G ** F is "1-1" ;
( 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_monomorphism U1,U3 by A9; :: thesis: verum