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 A2: ( F is injective & G is injective ) by FUNCTOR0:def 36;
A3: ( F is surjective & G is surjective ) by A1, FUNCTOR0:def 36;
A4: G * F is injective by A2, Th11;
G * F is surjective by A3, Th12;
hence G * F is bijective by A4, FUNCTOR0:def 36; :: thesis: verum