let A, B, C be non empty reflexive AltGraph ; :: thesis: for F1, F2 being feasible FunctorStr over A,B
for G1, G2 being FunctorStr over 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 over A,B; :: thesis: for G1, G2 being FunctorStr over 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 over 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 that
A1: FunctorStr(# the ObjectMap of F1, the MorphMap of F1 #) = FunctorStr(# the ObjectMap of F2, the MorphMap of F2 #) and
A2: FunctorStr(# the ObjectMap of G1, the MorphMap of G1 #) = FunctorStr(# the ObjectMap of G2, the MorphMap of G2 #) ; :: thesis: G1 * F1 = G2 * F2
A3: the ObjectMap of (G1 * F1) = the ObjectMap of G1 * the ObjectMap of F1 by FUNCTOR0:def 36;
the MorphMap of (G1 * F1) = ( the MorphMap of G1 * the ObjectMap of F1) ** the MorphMap of F1 by FUNCTOR0:def 36;
hence G1 * F1 = G2 * F2 by A1, A2, A3, FUNCTOR0:def 36; :: thesis: verum