let C1 be non empty AltGraph ; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( F is faithful & G is faithful implies G * F is faithful )
assume that
A1: F is faithful and
A2: G is faithful ; :: thesis: 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 ; :: thesis: ( 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:] ; :: thesis: 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; :: thesis: verum

end;

hence the MorphMap of (G * F) is "1-1" by MSUALG_3:1; :: according to FUNCTOR0:def 30 :: thesis: verum