for C1, C2, C3, C4, C5, C6 being category
for F1 being Functor of C1,C2
for F2 being Functor of C2,C3
for F3 being Functor of C1,C4
for F4 being Functor of C2,C5
for F5 being Functor of C3,C6
for F6 being Functor of C4,C5
for F7 being Functor of C5,C6 st F1 is covariant & F2 is covariant & F3 is covariant & F4 is covariant & F5 is covariant & F6 is covariant & F7 is covariant & C2,F2,F4 is_pullback_of F5,F7 holds
( C1,F1,F3 is_pullback_of F4,F6 iff ( C1,F2 (*) F1,F3 is_pullback_of F5,F7 (*) F6 & F4 (*) F1 = F6 (*) F3 ) )