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 surjective & G is surjective holds
G * F is surjective
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 surjective & G is surjective holds
G * F is surjective
let F be feasible FunctorStr of C1,C2; :: thesis: for G being FunctorStr of C2,C3 st F is surjective & G is surjective holds
G * F is surjective
let G be FunctorStr of C2,C3; :: thesis: ( F is surjective & G is surjective implies G * F is surjective )
assume A1: ( F is surjective & G is surjective ) ; :: thesis: G * F is surjective
then A2: ( F is full & G is full ) by FUNCTOR0:def 35;
A3: ( F is onto & G is onto ) by A1, FUNCTOR0:def 35;
A4: G * F is full by A2, Th10;
G * F is onto by A3, Th9;
hence G * F is surjective by A4, FUNCTOR0:def 35; :: thesis: verum