let C1, C2, C3, C4, C5, C6 be category; :: thesis: 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 ) )
let F1 be Functor of C1,C2; :: thesis: 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 ) )
let F2 be Functor of C2,C3; :: thesis: 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 ) )
let F3 be Functor of C1,C4; :: thesis: 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 ) )
let F4 be Functor of C2,C5; :: thesis: 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 ) )
let F5 be Functor of C3,C6; :: thesis: 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 ) )
let F6 be Functor of C4,C5; :: thesis: 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 ) )
let F7 be Functor of C5,C6; :: thesis: ( 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 implies ( C1,F1,F3 is_pullback_of F4,F6 iff ( C1,F2 (*) F1,F3 is_pullback_of F5,F7 (*) F6 & F4 (*) F1 = F6 (*) F3 ) ) )
assume A1: ( F1 is covariant & F2 is covariant & F3 is covariant & F4 is covariant & F5 is covariant & F6 is covariant & F7 is covariant ) ; :: thesis: ( not C2,F2,F4 is_pullback_of F5,F7 or ( C1,F1,F3 is_pullback_of F4,F6 iff ( C1,F2 (*) F1,F3 is_pullback_of F5,F7 (*) F6 & F4 (*) F1 = F6 (*) F3 ) ) )
assume A2: C2,F2,F4 is_pullback_of F5,F7 ; :: thesis: ( C1,F1,F3 is_pullback_of F4,F6 iff ( C1,F2 (*) F1,F3 is_pullback_of F5,F7 (*) F6 & F4 (*) F1 = F6 (*) F3 ) )
then A3: ( F5 (*) F2 = F7 (*) F4 & ( for D1 being category
for G1 being Functor of D1,C3
for G2 being Functor of D1,C5 st G1 is covariant & G2 is covariant & F5 (*) G1 = F7 (*) G2 holds
ex H being Functor of D1,C2 st
( H is covariant & F2 (*) H = G1 & F4 (*) H = G2 & ( for H1 being Functor of D1,C2 st H1 is covariant & F2 (*) H1 = G1 & F4 (*) H1 = G2 holds
H = H1 ) ) ) ) by A1, Def20;

hereby :: thesis: ( C1,F2 (*) F1,F3 is_pullback_of F5,F7 (*) F6 & F4 (*) F1 = F6 (*) F3 implies C1,F1,F3 is_pullback_of F4,F6 )

assume A4: C1,F1,F3 is_pullback_of F4,F6 ; :: thesis: ( C1,F2 (*) F1,F3 is_pullback_of F5,F7 (*) F6 & F4 (*) F1 = F6 (*) F3 )
then A5: ( F4 (*) F1 = F6 (*) F3 & ( for D1 being category
for G1 being Functor of D1,C2
for G2 being Functor of D1,C4 st G1 is covariant & G2 is covariant & F4 (*) G1 = F6 (*) G2 holds
ex H being Functor of D1,C1 st
( H is covariant & F1 (*) H = G1 & F3 (*) H = G2 & ( for H1 being Functor of D1,C1 st H1 is covariant & F1 (*) H1 = G1 & F3 (*) H1 = G2 holds
H = H1 ) ) ) ) by A1, Def20;
A6: ( F7 (*) F6 is covariant & F2 (*) F1 is covariant & F3 is covariant ) by A1, CAT_6:35;
A7: F5 (*) (F2 (*) F1) = (F5 (*) F2) (*) F1 by A1, Th10
.= F7 (*) (F6 (*) F3) by A3, A5, Th10, A1
.= (F7 (*) F6) (*) F3 by A1, Th10 ;
for D1 being category
for G1 being Functor of D1,C3
for G2 being Functor of D1,C4 st G1 is covariant & G2 is covariant & F5 (*) G1 = (F7 (*) F6) (*) G2 holds
ex H being Functor of D1,C1 st
( H is covariant & (F2 (*) F1) (*) H = G1 & F3 (*) H = G2 & ( for H1 being Functor of D1,C1 st H1 is covariant & (F2 (*) F1) (*) H1 = G1 & F3 (*) H1 = G2 holds
H = H1 ) )

proof

let D1 be category; :: thesis: for G1 being Functor of D1,C3
for G2 being Functor of D1,C4 st G1 is covariant & G2 is covariant & F5 (*) G1 = (F7 (*) F6) (*) G2 holds
ex H being Functor of D1,C1 st
( H is covariant & (F2 (*) F1) (*) H = G1 & F3 (*) H = G2 & ( for H1 being Functor of D1,C1 st H1 is covariant & (F2 (*) F1) (*) H1 = G1 & F3 (*) H1 = G2 holds
H = H1 ) )
let G1 be Functor of D1,C3; :: thesis: for G2 being Functor of D1,C4 st G1 is covariant & G2 is covariant & F5 (*) G1 = (F7 (*) F6) (*) G2 holds
ex H being Functor of D1,C1 st
( H is covariant & (F2 (*) F1) (*) H = G1 & F3 (*) H = G2 & ( for H1 being Functor of D1,C1 st H1 is covariant & (F2 (*) F1) (*) H1 = G1 & F3 (*) H1 = G2 holds
H = H1 ) )
let G2 be Functor of D1,C4; :: thesis: ( G1 is covariant & G2 is covariant & F5 (*) G1 = (F7 (*) F6) (*) G2 implies ex H being Functor of D1,C1 st
( H is covariant & (F2 (*) F1) (*) H = G1 & F3 (*) H = G2 & ( for H1 being Functor of D1,C1 st H1 is covariant & (F2 (*) F1) (*) H1 = G1 & F3 (*) H1 = G2 holds
H = H1 ) ) )
assume A8: G1 is covariant ; :: thesis: ( not G2 is covariant or not F5 (*) G1 = (F7 (*) F6) (*) G2 or ex H being Functor of D1,C1 st
( H is covariant & (F2 (*) F1) (*) H = G1 & F3 (*) H = G2 & ( for H1 being Functor of D1,C1 st H1 is covariant & (F2 (*) F1) (*) H1 = G1 & F3 (*) H1 = G2 holds
H = H1 ) ) )
assume A9: G2 is covariant ; :: thesis: ( not F5 (*) G1 = (F7 (*) F6) (*) G2 or ex H being Functor of D1,C1 st
( H is covariant & (F2 (*) F1) (*) H = G1 & F3 (*) H = G2 & ( for H1 being Functor of D1,C1 st H1 is covariant & (F2 (*) F1) (*) H1 = G1 & F3 (*) H1 = G2 holds
H = H1 ) ) )
assume A10: F5 (*) G1 = (F7 (*) F6) (*) G2 ; :: thesis: ex H being Functor of D1,C1 st
( H is covariant & (F2 (*) F1) (*) H = G1 & F3 (*) H = G2 & ( for H1 being Functor of D1,C1 st H1 is covariant & (F2 (*) F1) (*) H1 = G1 & F3 (*) H1 = G2 holds
H = H1 ) )
A11: F6 (*) G2 is covariant by A1, A9, CAT_6:35;
A12: F5 (*) G1 = F7 (*) (F6 (*) G2) by A10, A9, A1, Th10;
consider G3 being Functor of D1,C2 such that
A13: ( G3 is covariant & F2 (*) G3 = G1 & F4 (*) G3 = F6 (*) G2 & ( for H1 being Functor of D1,C2 st H1 is covariant & F2 (*) H1 = G1 & F4 (*) H1 = F6 (*) G2 holds
G3 = H1 ) ) by A11, A12, A2, A8, A1, Def20;
consider H being Functor of D1,C1 such that
A14: ( H is covariant & F1 (*) H = G3 & F3 (*) H = G2 & ( for H1 being Functor of D1,C1 st H1 is covariant & F1 (*) H1 = G3 & F3 (*) H1 = G2 holds
H = H1 ) ) by A13, A9, A4, A1, Def20;
take H ; :: thesis: ( H is covariant & (F2 (*) F1) (*) H = G1 & F3 (*) H = G2 & ( for H1 being Functor of D1,C1 st H1 is covariant & (F2 (*) F1) (*) H1 = G1 & F3 (*) H1 = G2 holds
H = H1 ) )
thus H is covariant by A14; :: thesis: ( (F2 (*) F1) (*) H = G1 & F3 (*) H = G2 & ( for H1 being Functor of D1,C1 st H1 is covariant & (F2 (*) F1) (*) H1 = G1 & F3 (*) H1 = G2 holds
H = H1 ) )
thus (F2 (*) F1) (*) H = G1 by A1, A13, A14, Th10; :: thesis: ( F3 (*) H = G2 & ( for H1 being Functor of D1,C1 st H1 is covariant & (F2 (*) F1) (*) H1 = G1 & F3 (*) H1 = G2 holds
H = H1 ) )
thus F3 (*) H = G2 by A14; :: thesis: for H1 being Functor of D1,C1 st H1 is covariant & (F2 (*) F1) (*) H1 = G1 & F3 (*) H1 = G2 holds
H = H1
let H1 be Functor of D1,C1; :: thesis: ( H1 is covariant & (F2 (*) F1) (*) H1 = G1 & F3 (*) H1 = G2 implies H = H1 )
assume A15: H1 is covariant ; :: thesis: ( not (F2 (*) F1) (*) H1 = G1 or not F3 (*) H1 = G2 or H = H1 )
assume A16: (F2 (*) F1) (*) H1 = G1 ; :: thesis: ( not F3 (*) H1 = G2 or H = H1 )
assume A17: F3 (*) H1 = G2 ; :: thesis: H = H1
A18: F2 (*) (F1 (*) H1) = G1 by A1, A15, A16, Th10;
F4 (*) (F1 (*) H1) = (F4 (*) F1) (*) H1 by A1, A15, Th10
.= F6 (*) G2 by A15, A17, A5, Th10, A1 ;
then G3 = F1 (*) H1 by A18, A13, A1, A15, CAT_6:35;
hence H = H1 by A15, A17, A14; :: thesis: verum

end;

hence C1,F2 (*) F1,F3 is_pullback_of F5,F7 (*) F6 by A6, A1, A7, Def20; :: thesis: F4 (*) F1 = F6 (*) F3
thus F4 (*) F1 = F6 (*) F3 by A4, A1, Def20; :: thesis: verum

end;

A19: ( F7 (*) F6 is covariant & F2 (*) F1 is covariant ) by A1, CAT_6:35;
assume A20: C1,F2 (*) F1,F3 is_pullback_of F5,F7 (*) F6 ; :: thesis: ( not F4 (*) F1 = F6 (*) F3 or C1,F1,F3 is_pullback_of F4,F6 )
assume A21: F4 (*) F1 = F6 (*) F3 ; :: thesis: C1,F1,F3 is_pullback_of F4,F6
for D1 being category
for G1 being Functor of D1,C2
for G2 being Functor of D1,C4 st G1 is covariant & G2 is covariant & F4 (*) G1 = F6 (*) G2 holds
ex H being Functor of D1,C1 st
( H is covariant & F1 (*) H = G1 & F3 (*) H = G2 & ( for H1 being Functor of D1,C1 st H1 is covariant & F1 (*) H1 = G1 & F3 (*) H1 = G2 holds
H = H1 ) )

proof

let D1 be category; :: thesis: for G1 being Functor of D1,C2
for G2 being Functor of D1,C4 st G1 is covariant & G2 is covariant & F4 (*) G1 = F6 (*) G2 holds
ex H being Functor of D1,C1 st
( H is covariant & F1 (*) H = G1 & F3 (*) H = G2 & ( for H1 being Functor of D1,C1 st H1 is covariant & F1 (*) H1 = G1 & F3 (*) H1 = G2 holds
H = H1 ) )
let G1 be Functor of D1,C2; :: thesis: for G2 being Functor of D1,C4 st G1 is covariant & G2 is covariant & F4 (*) G1 = F6 (*) G2 holds
ex H being Functor of D1,C1 st
( H is covariant & F1 (*) H = G1 & F3 (*) H = G2 & ( for H1 being Functor of D1,C1 st H1 is covariant & F1 (*) H1 = G1 & F3 (*) H1 = G2 holds
H = H1 ) )
let G2 be Functor of D1,C4; :: thesis: ( G1 is covariant & G2 is covariant & F4 (*) G1 = F6 (*) G2 implies ex H being Functor of D1,C1 st
( H is covariant & F1 (*) H = G1 & F3 (*) H = G2 & ( for H1 being Functor of D1,C1 st H1 is covariant & F1 (*) H1 = G1 & F3 (*) H1 = G2 holds
H = H1 ) ) )
assume A22: G1 is covariant ; :: thesis: ( not G2 is covariant or not F4 (*) G1 = F6 (*) G2 or ex H being Functor of D1,C1 st
( H is covariant & F1 (*) H = G1 & F3 (*) H = G2 & ( for H1 being Functor of D1,C1 st H1 is covariant & F1 (*) H1 = G1 & F3 (*) H1 = G2 holds
H = H1 ) ) )
assume A23: G2 is covariant ; :: thesis: ( not F4 (*) G1 = F6 (*) G2 or ex H being Functor of D1,C1 st
( H is covariant & F1 (*) H = G1 & F3 (*) H = G2 & ( for H1 being Functor of D1,C1 st H1 is covariant & F1 (*) H1 = G1 & F3 (*) H1 = G2 holds
H = H1 ) ) )
assume A24: F4 (*) G1 = F6 (*) G2 ; :: thesis: ex H being Functor of D1,C1 st
( H is covariant & F1 (*) H = G1 & F3 (*) H = G2 & ( for H1 being Functor of D1,C1 st H1 is covariant & F1 (*) H1 = G1 & F3 (*) H1 = G2 holds
H = H1 ) )
set G11 = F2 (*) G1;
A25: F2 (*) G1 is covariant by A1, A22, CAT_6:35;
A26: F5 (*) (F2 (*) G1) = (F5 (*) F2) (*) G1 by A22, A1, Th10
.= F7 (*) (F6 (*) G2) by A24, A22, A3, Th10, A1
.= (F7 (*) F6) (*) G2 by A23, A1, Th10 ;
consider H being Functor of D1,C1 such that
A27: ( H is covariant & (F2 (*) F1) (*) H = F2 (*) G1 & F3 (*) H = G2 & ( for H1 being Functor of D1,C1 st H1 is covariant & (F2 (*) F1) (*) H1 = F2 (*) G1 & F3 (*) H1 = G2 holds
H = H1 ) ) by A1, A26, A23, A25, A20, A19, Def20;
take H ; :: thesis: ( H is covariant & F1 (*) H = G1 & F3 (*) H = G2 & ( for H1 being Functor of D1,C1 st H1 is covariant & F1 (*) H1 = G1 & F3 (*) H1 = G2 holds
H = H1 ) )
thus H is covariant by A27; :: thesis: ( F1 (*) H = G1 & F3 (*) H = G2 & ( for H1 being Functor of D1,C1 st H1 is covariant & F1 (*) H1 = G1 & F3 (*) H1 = G2 holds
H = H1 ) )
set G22 = F4 (*) G1;
A28: ( F2 (*) G1 is covariant & F4 (*) G1 is covariant ) by A1, A22, CAT_6:35;
A29: F5 (*) (F2 (*) G1) = (F5 (*) F2) (*) G1 by A22, A1, Th10
.= F7 (*) (F4 (*) G1) by A22, A3, Th10, A1 ;
consider H2 being Functor of D1,C2 such that
A30: ( H2 is covariant & F2 (*) H2 = F2 (*) G1 & F4 (*) H2 = F4 (*) G1 & ( for H1 being Functor of D1,C2 st H1 is covariant & F2 (*) H1 = F2 (*) G1 & F4 (*) H1 = F4 (*) G1 holds
H2 = H1 ) ) by A29, A28, A2, A1, Def20;
A31: H2 = G1 by A22, A30;
A32: F2 (*) (F1 (*) H) = F2 (*) G1 by A1, A27, Th10;
F4 (*) (F1 (*) H) = (F4 (*) F1) (*) H by A1, A27, Th10
.= F4 (*) G1 by A27, A24, A21, A1, Th10 ;
hence F1 (*) H = G1 by A30, A32, A31, A1, A27, CAT_6:35; :: thesis: ( F3 (*) H = G2 & ( for H1 being Functor of D1,C1 st H1 is covariant & F1 (*) H1 = G1 & F3 (*) H1 = G2 holds
H = H1 ) )
thus F3 (*) H = G2 by A27; :: thesis: for H1 being Functor of D1,C1 st H1 is covariant & F1 (*) H1 = G1 & F3 (*) H1 = G2 holds
H = H1
let H1 be Functor of D1,C1; :: thesis: ( H1 is covariant & F1 (*) H1 = G1 & F3 (*) H1 = G2 implies H = H1 )
assume A33: H1 is covariant ; :: thesis: ( not F1 (*) H1 = G1 or not F3 (*) H1 = G2 or H = H1 )
assume A34: F1 (*) H1 = G1 ; :: thesis: ( not F3 (*) H1 = G2 or H = H1 )
A35: (F2 (*) F1) (*) H1 = F2 (*) G1 by A1, A33, A34, Th10;
assume F3 (*) H1 = G2 ; :: thesis: H = H1
hence H = H1 by A33, A27, A35; :: thesis: verum

end;

hence C1,F1,F3 is_pullback_of F4,F6 by A21, A1, Def20; :: thesis: verum