let C1 be non empty AltGraph ; :: thesis: for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr of C1,C2
for G being FunctorStr of 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 of C1,C2
for G being FunctorStr of C2,C3 st F is faithful & G is faithful holds
G * F is faithful
let F be feasible FunctorStr of C1,C2; :: thesis: for G being FunctorStr of C2,C3 st F is faithful & G is faithful holds
G * F is faithful
let G be FunctorStr of C2,C3; :: thesis: ( F is faithful & G is faithful implies G * F is faithful )
assume A1: ( F is faithful & G is faithful ) ; :: thesis: G * F is faithful
set CC1 = [:the carrier of C1,the carrier of C1:];
set CC2 = [:the carrier of C2,the carrier of C2:];
set MMF = the MorphMap of F;
set MMG = the MorphMap of G;
reconsider MMGF = the MorphMap of (G * F) as ManySortedFunction of ;
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:] ;
A2: ( the MorphMap of F is "1-1" & the MorphMap of G is "1-1" ) by A1, FUNCTOR0:def 31;
A3: MMGF = (the MorphMap of G * OMF) ** the MorphMap of F by FUNCTOR0:def 37;
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 A4: i in [:the carrier of C1,the carrier of C1:] ; :: thesis: MMGF . i is one-to-one
then A5: OMF . i in [:the carrier of C2,the carrier of C2:] by FUNCT_2:7;
i in dom ((the MorphMap of G * OMF) ** the MorphMap of F) by A4, PARTFUN1:def 4;
then A6: MMGF . i = ((the MorphMap of G * OMF) . i) * (the MorphMap of F . i) by A3, PBOOLE:def 24
.= (the MorphMap of G . (OMF . i)) * (the MorphMap of F . i) by A4, FUNCT_2:21 ;
A7: the MorphMap of G . (OMF . i) is one-to-one by A2, A5, MSUALG_3:1;
the MorphMap of F . i is one-to-one by A2, A4, MSUALG_3:1;
hence MMGF . i is one-to-one by A6, A7; :: thesis: verum

end;

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