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 injective & G is injective holds
G * F is injective
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 injective & G is injective holds
G * F is injective
let F be feasible FunctorStr of C1,C2; :: thesis: for G being FunctorStr of C2,C3 st F is injective & G is injective holds
G * F is injective
let G be FunctorStr of C2,C3; :: thesis: ( F is injective & G is injective implies G * F is injective )
assume A1: ( F is injective & G is injective ) ; :: thesis: G * F is injective
then ( F is faithful & G is faithful ) by FUNCTOR0:def 33;
then A2: G * F is faithful by Th8;
( F is one-to-one & G is one-to-one ) by A1, FUNCTOR0:def 33;
then G * F is one-to-one by Th7;
hence G * F is injective by A2, FUNCTOR0:def 33; :: thesis: verum