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
[|F1,F2|] ~= [|F2,F1|]
let F1 be Functor of C1,C; :: thesis: for F2 being Functor of C2,C st F1 is covariant & F2 is covariant holds
[|F1,F2|] ~= [|F2,F1|]
let F2 be Functor of C2,C; :: thesis: ( F1 is covariant & F2 is covariant implies [|F1,F2|] ~= [|F2,F1|] )
assume A1: ( F1 is covariant & F2 is covariant ) ; :: thesis: [|F1,F2|] ~= [|F2,F1|]
A2: ( 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, Th52;
A3: ( pr1 (F2,F1) is covariant & pr2 (F2,F1) is covariant & [|F2,F1|], pr1 (F2,F1), pr2 (F2,F1) is_pullback_of F2,F1 ) by A1, Th52;
then [|F2,F1|], pr2 (F2,F1), pr1 (F2,F1) is_pullback_of F1,F2 by A1, Th47;
hence [|F1,F2|] ~= [|F2,F1|] by A1, A2, A3, Th46; :: thesis: verum