let C1 be non empty AltGraph ; for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3 st F is faithful & G is faithful holds
G * F is faithful
let C2, C3 be non empty reflexive AltGraph ; for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3 st F is faithful & G is faithful holds
G * F is faithful
let F be feasible FunctorStr over C1,C2; for G being FunctorStr over C2,C3 st F is faithful & G is faithful holds
G * F is faithful
let G be FunctorStr over C2,C3; ( F is faithful & G is faithful implies G * F is faithful )
assume that
A1:
F is faithful
and
A2:
G is faithful
; G * F is faithful
set MMG = the MorphMap of G;
A3:
the MorphMap of G is "1-1"
by A2;
set MMF = the MorphMap of F;
set CC2 = [: the carrier of C2, the carrier of C2:];
set CC1 = [: the carrier of C1, the carrier of C1:];
reconsider MMGF = the MorphMap of (G * F) as ManySortedFunction of [: the carrier of C1, the carrier of C1:] ;
reconsider OMF = the ObjectMap of F as Function of [: the carrier of C1, the carrier of C1:],[: the carrier of C2, the carrier of C2:] ;
A4:
MMGF = ( the MorphMap of G * OMF) ** the MorphMap of F
by FUNCTOR0:def 36;
A5:
the MorphMap of F is "1-1"
by A1;
for i being set st i in [: the carrier of C1, the carrier of C1:] holds
MMGF . i is one-to-one
proof
let i be
set ;
( i in [: the carrier of C1, the carrier of C1:] implies MMGF . i is one-to-one )
assume A6:
i in [: the carrier of C1, the carrier of C1:]
;
MMGF . i is one-to-one
then
i in dom (( the MorphMap of G * OMF) ** the MorphMap of F)
by PARTFUN1:def 2;
then A7:
MMGF . i =
(( the MorphMap of G * OMF) . i) * ( the MorphMap of F . i)
by A4, PBOOLE:def 19
.=
( the MorphMap of G . (OMF . i)) * ( the MorphMap of F . i)
by A6, FUNCT_2:15
;
OMF . i in [: the carrier of C2, the carrier of C2:]
by A6, FUNCT_2:5;
then A8:
the
MorphMap of
G . (OMF . i) is
one-to-one
by A3, MSUALG_3:1;
the
MorphMap of
F . i is
one-to-one
by A5, A6, MSUALG_3:1;
hence
MMGF . i is
one-to-one
by A7, A8;
verum
end;
hence
the MorphMap of (G * F) is "1-1"
by MSUALG_3:1; FUNCTOR0:def 30 verum