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

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