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 bijective & G is bijective holds
G * F is bijective
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 bijective & G is bijective holds
G * F is bijective
let F be feasible FunctorStr of C1,C2; :: thesis: for G being FunctorStr of C2,C3 st F is bijective & G is bijective holds
G * F is bijective
let G be FunctorStr of C2,C3; :: thesis: ( F is bijective & G is bijective implies G * F is bijective )
assume A1: ( F is bijective & G is bijective ) ; :: thesis: G * F is bijective
then ( F is surjective & G is surjective ) by FUNCTOR0:def 36;
then A2: G * F is surjective by Th12;
( F is injective & G is injective ) by A1, FUNCTOR0:def 36;
then G * F is injective by Th11;
hence G * F is bijective by A2, FUNCTOR0:def 36; :: thesis: verum