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

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

hence
the MorphMap of (G * F) is "1-1"
by MSUALG_3:1; :: according to FUNCTOR0:def 30 :: thesis: verum
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;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