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

( 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

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

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

( 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