let S be non empty non void ManySortedSign ; for U1, U2, U3 being non-empty MSAlgebra of 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 of 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 F be 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 G be ManySortedFunction of U2,U3; ( 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
; G ** F is_monomorphism U1,U3
A3:
G is "1-1"
by A2, Def11;
A4:
F is "1-1"
by A1, Def11;
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 ;
for h being Function st i in dom (G ** F) & (G ** F) . i = h holds
h is one-to-one let h be
Function;
( 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
;
h is one-to-one
A7:
i in the
carrier of
S
by A5, PARTFUN1:def 4;
then reconsider g =
G . i as
Function of
( the Sorts of U2 . i),
( the Sorts of U3 . i) by PBOOLE:def 18;
reconsider f =
F . i as
Function of
( the Sorts of U1 . i),
( the Sorts of U2 . i) by A7, PBOOLE:def 18;
i in dom G
by A7, PARTFUN1:def 4;
then A8:
g is
one-to-one
by A3, Def2;
i in dom F
by A7, PARTFUN1:def 4;
then
f is
one-to-one
by A4, Def2;
then
g * f is
one-to-one
by A8;
hence
h is
one-to-one
by A6, A7, Th2;
verum
end;
then A9:
G ** F is "1-1"
by Def2;
( F is_homomorphism U1,U2 & G is_homomorphism U2,U3 )
by A1, A2, Def11;
then
G ** F is_homomorphism U1,U3
by Th10;
hence
G ** F is_monomorphism U1,U3
by A9, Def11; verum