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