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 one-to-one & G is one-to-one holds

G * F is one-to-one

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 one-to-one & G is one-to-one holds

G * F is one-to-one

let F be feasible FunctorStr over C1,C2; :: thesis: for G being FunctorStr over C2,C3 st F is one-to-one & G is one-to-one holds

G * F is one-to-one

let G be FunctorStr over C2,C3; :: thesis: ( F is one-to-one & G is one-to-one implies G * F is one-to-one )

assume ( F is one-to-one & G is one-to-one ) ; :: thesis: G * F is one-to-one

then A1: ( the ObjectMap of F is one-to-one & the ObjectMap of G is one-to-one ) ;

the ObjectMap of (G * F) = the ObjectMap of G * the ObjectMap of F by FUNCTOR0:def 36;

hence the ObjectMap of (G * F) is one-to-one by A1; :: according to FUNCTOR0:def 6 :: thesis: verum

for F being feasible FunctorStr over C1,C2

for G being FunctorStr over C2,C3 st F is one-to-one & G is one-to-one holds

G * F is one-to-one

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 one-to-one & G is one-to-one holds

G * F is one-to-one

let F be feasible FunctorStr over C1,C2; :: thesis: for G being FunctorStr over C2,C3 st F is one-to-one & G is one-to-one holds

G * F is one-to-one

let G be FunctorStr over C2,C3; :: thesis: ( F is one-to-one & G is one-to-one implies G * F is one-to-one )

assume ( F is one-to-one & G is one-to-one ) ; :: thesis: G * F is one-to-one

then A1: ( the ObjectMap of F is one-to-one & the ObjectMap of G is one-to-one ) ;

the ObjectMap of (G * F) = the ObjectMap of G * the ObjectMap of F by FUNCTOR0:def 36;

hence the ObjectMap of (G * F) is one-to-one by A1; :: according to FUNCTOR0:def 6 :: thesis: verum