let A, B, C be non empty reflexive AltGraph ; :: thesis: for F1, F2 being feasible FunctorStr of A,B
for G1, G2 being FunctorStr of B,C st FunctorStr(# the ObjectMap of F1,the MorphMap of F1 #) = FunctorStr(# the ObjectMap of F2,the MorphMap of F2 #) & FunctorStr(# the ObjectMap of G1,the MorphMap of G1 #) = FunctorStr(# the ObjectMap of G2,the MorphMap of G2 #) holds
G1 * F1 = G2 * F2
let F1, F2 be feasible FunctorStr of A,B; :: thesis: for G1, G2 being FunctorStr of B,C st FunctorStr(# the ObjectMap of F1,the MorphMap of F1 #) = FunctorStr(# the ObjectMap of F2,the MorphMap of F2 #) & FunctorStr(# the ObjectMap of G1,the MorphMap of G1 #) = FunctorStr(# the ObjectMap of G2,the MorphMap of G2 #) holds
G1 * F1 = G2 * F2
let G1, G2 be FunctorStr of B,C; :: thesis: ( FunctorStr(# the ObjectMap of F1,the MorphMap of F1 #) = FunctorStr(# the ObjectMap of F2,the MorphMap of F2 #) & FunctorStr(# the ObjectMap of G1,the MorphMap of G1 #) = FunctorStr(# the ObjectMap of G2,the MorphMap of G2 #) implies G1 * F1 = G2 * F2 )
assume A1: ( FunctorStr(# the ObjectMap of F1,the MorphMap of F1 #) = FunctorStr(# the ObjectMap of F2,the MorphMap of F2 #) & FunctorStr(# the ObjectMap of G1,the MorphMap of G1 #) = FunctorStr(# the ObjectMap of G2,the MorphMap of G2 #) ) ; :: thesis: G1 * F1 = G2 * F2
( the ObjectMap of (G1 * F1) = the ObjectMap of G1 * the ObjectMap of F1 & the MorphMap of (G1 * F1) = (the MorphMap of G1 * the ObjectMap of F1) ** the MorphMap of F1 ) by FUNCTOR0:def 37;
hence G1 * F1 = G2 * F2 by A1, FUNCTOR0:def 37; :: thesis: verum