let C, C1, C2 be category; :: thesis: for F1 being Functor of C1,C
for F2 being Functor of C2,C st F1 is covariant & F2 is covariant holds
( pr1 (F1,F2) is covariant & pr2 (F1,F2) is covariant & [|F1,F2|], pr1 (F1,F2), pr2 (F1,F2) is_pullback_of F1,F2 )
let F1 be Functor of C1,C; :: thesis: for F2 being Functor of C2,C st F1 is covariant & F2 is covariant holds
( pr1 (F1,F2) is covariant & pr2 (F1,F2) is covariant & [|F1,F2|], pr1 (F1,F2), pr2 (F1,F2) is_pullback_of F1,F2 )
let F2 be Functor of C2,C; :: thesis: ( F1 is covariant & F2 is covariant implies ( pr1 (F1,F2) is covariant & pr2 (F1,F2) is covariant & [|F1,F2|], pr1 (F1,F2), pr2 (F1,F2) is_pullback_of F1,F2 ) )
assume A1: ( F1 is covariant & F2 is covariant ) ; :: thesis: ( pr1 (F1,F2) is covariant & pr2 (F1,F2) is covariant & [|F1,F2|], pr1 (F1,F2), pr2 (F1,F2) is_pullback_of F1,F2 )
set T = the pullback of F1,F2;
consider D0 being strict category, P01 being Functor of D0,C1, P02 being Functor of D0,C2 such that
A2: ( the pullback of F1,F2 = [D0,P01,P02] & P01 is covariant & P02 is covariant & D0,P01,P02 is_pullback_of F1,F2 ) by A1, Def21;
A3: ( F1 (*) P01 = F2 (*) P02 & ( for D1 being category
for G1 being Functor of D1,C1
for G2 being Functor of D1,C2 st G1 is covariant & G2 is covariant & F1 (*) G1 = F2 (*) G2 holds
ex H being Functor of D1,D0 st
( H is covariant & P01 (*) H = G1 & P02 (*) H = G2 & ( for H1 being Functor of D1,D0 st H1 is covariant & P01 (*) H1 = G1 & P02 (*) H1 = G2 holds
H = H1 ) ) ) ) by A1, A2, Def20;
A4: ( [D0,P01,P02] `1_3 = D0 & [D0,P01,P02] `2_3 = P01 & [D0,P01,P02] `3_3 = P02 ) ;
then A5: D0 = [|F1,F2|] by A1, A2, Def22;
reconsider P1 = P01 as Functor of [|F1,F2|],C1 by A5;
reconsider P2 = P02 as Functor of [|F1,F2|],C2 by A5;
( pr1 (F1,F2) is covariant & pr2 (F1,F2) is covariant & F1 (*) (pr1 (F1,F2)) = F2 (*) (pr2 (F1,F2)) & ( for D1 being category
for G1 being Functor of D1,C1
for G2 being Functor of D1,C2 st G1 is covariant & G2 is covariant & F1 (*) G1 = F2 (*) G2 holds
ex H being Functor of D1,[|F1,F2|] st
( H is covariant & (pr1 (F1,F2)) (*) H = G1 & (pr2 (F1,F2)) (*) H = G2 & ( for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds
H = H1 ) ) ) )

proof

thus A6: pr1 (F1,F2) is covariant by A2, A5, A4, A1, Def23; :: thesis: ( pr2 (F1,F2) is covariant & F1 (*) (pr1 (F1,F2)) = F2 (*) (pr2 (F1,F2)) & ( for D1 being category
for G1 being Functor of D1,C1
for G2 being Functor of D1,C2 st G1 is covariant & G2 is covariant & F1 (*) G1 = F2 (*) G2 holds
ex H being Functor of D1,[|F1,F2|] st
( H is covariant & (pr1 (F1,F2)) (*) H = G1 & (pr2 (F1,F2)) (*) H = G2 & ( for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds
H = H1 ) ) ) )
thus A7: pr2 (F1,F2) is covariant by A2, A5, A4, A1, Def24; :: thesis: ( F1 (*) (pr1 (F1,F2)) = F2 (*) (pr2 (F1,F2)) & ( for D1 being category
for G1 being Functor of D1,C1
for G2 being Functor of D1,C2 st G1 is covariant & G2 is covariant & F1 (*) G1 = F2 (*) G2 holds
ex H being Functor of D1,[|F1,F2|] st
( H is covariant & (pr1 (F1,F2)) (*) H = G1 & (pr2 (F1,F2)) (*) H = G2 & ( for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds
H = H1 ) ) ) )
thus F1 (*) (pr1 (F1,F2)) = (pr1 (F1,F2)) * F1 by A6, A1, CAT_6:def 27
.= P01 * F1 by A4, A2, A1, Def23
.= F1 (*) P01 by A2, A1, CAT_6:def 27
.= P02 * F2 by A2, A1, A3, CAT_6:def 27
.= (pr2 (F1,F2)) * F2 by A4, A2, A1, Def24
.= F2 (*) (pr2 (F1,F2)) by A7, A1, CAT_6:def 27 ; :: thesis: for D1 being category
for G1 being Functor of D1,C1
for G2 being Functor of D1,C2 st G1 is covariant & G2 is covariant & F1 (*) G1 = F2 (*) G2 holds
ex H being Functor of D1,[|F1,F2|] st
( H is covariant & (pr1 (F1,F2)) (*) H = G1 & (pr2 (F1,F2)) (*) H = G2 & ( for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds
H = H1 ) )
let D1 be category; :: thesis: for G1 being Functor of D1,C1
for G2 being Functor of D1,C2 st G1 is covariant & G2 is covariant & F1 (*) G1 = F2 (*) G2 holds
ex H being Functor of D1,[|F1,F2|] st
( H is covariant & (pr1 (F1,F2)) (*) H = G1 & (pr2 (F1,F2)) (*) H = G2 & ( for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds
H = H1 ) )
let G1 be Functor of D1,C1; :: thesis: for G2 being Functor of D1,C2 st G1 is covariant & G2 is covariant & F1 (*) G1 = F2 (*) G2 holds
ex H being Functor of D1,[|F1,F2|] st
( H is covariant & (pr1 (F1,F2)) (*) H = G1 & (pr2 (F1,F2)) (*) H = G2 & ( for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds
H = H1 ) )
let G2 be Functor of D1,C2; :: thesis: ( G1 is covariant & G2 is covariant & F1 (*) G1 = F2 (*) G2 implies ex H being Functor of D1,[|F1,F2|] st
( H is covariant & (pr1 (F1,F2)) (*) H = G1 & (pr2 (F1,F2)) (*) H = G2 & ( for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds
H = H1 ) ) )
assume ( G1 is covariant & G2 is covariant & F1 (*) G1 = F2 (*) G2 ) ; :: thesis: ex H being Functor of D1,[|F1,F2|] st
( H is covariant & (pr1 (F1,F2)) (*) H = G1 & (pr2 (F1,F2)) (*) H = G2 & ( for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds
H = H1 ) )
then consider H0 being Functor of D1,D0 such that
A8: ( H0 is covariant & P01 (*) H0 = G1 & P02 (*) H0 = G2 & ( for H1 being Functor of D1,D0 st H1 is covariant & P01 (*) H1 = G1 & P02 (*) H1 = G2 holds
H0 = H1 ) ) by A1, A2, Def20;
reconsider H = H0 as Functor of D1,[|F1,F2|] by A5;
take H ; :: thesis: ( H is covariant & (pr1 (F1,F2)) (*) H = G1 & (pr2 (F1,F2)) (*) H = G2 & ( for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds
H = H1 ) )
thus H is covariant by A5, A8; :: thesis: ( (pr1 (F1,F2)) (*) H = G1 & (pr2 (F1,F2)) (*) H = G2 & ( for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds
H = H1 ) )
thus (pr1 (F1,F2)) (*) H = H * (pr1 (F1,F2)) by A5, A8, A6, CAT_6:def 27
.= H0 * P01 by A4, A2, A1, Def23
.= G1 by A2, A8, CAT_6:def 27 ; :: thesis: ( (pr2 (F1,F2)) (*) H = G2 & ( for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds
H = H1 ) )
thus (pr2 (F1,F2)) (*) H = H * (pr2 (F1,F2)) by A5, A8, A7, CAT_6:def 27
.= H0 * P02 by A4, A2, A1, Def24
.= G2 by A2, A8, CAT_6:def 27 ; :: thesis: for H1 being Functor of D1,[|F1,F2|] st H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 holds
H = H1
let H1 be Functor of D1,[|F1,F2|]; :: thesis: ( H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 implies H = H1 )
assume A9: ( H1 is covariant & (pr1 (F1,F2)) (*) H1 = G1 & (pr2 (F1,F2)) (*) H1 = G2 ) ; :: thesis: H = H1
reconsider H01 = H1 as Functor of D1,D0 by A5;
A10: P01 (*) H01 = H01 * P01 by A2, A9, A5, CAT_6:def 27
.= H1 * (pr1 (F1,F2)) by A4, A2, A1, Def23
.= G1 by A9, A6, CAT_6:def 27 ;
P02 (*) H01 = H01 * P02 by A2, A9, A5, CAT_6:def 27
.= H1 * (pr2 (F1,F2)) by A4, A2, A1, Def24
.= G2 by A9, A7, CAT_6:def 27 ;
hence H = H1 by A8, A9, A5, A10; :: thesis: verum

end;

hence ( pr1 (F1,F2) is covariant & pr2 (F1,F2) is covariant & [|F1,F2|], pr1 (F1,F2), pr2 (F1,F2) is_pullback_of F1,F2 ) by A1, Def20; :: thesis: verum