let C1, C2 be non empty category; :: thesis: for f1, g1 being morphism of C1
for f2, g2 being morphism of C2 st f1 |> g1 & f2 |> g2 holds
[f1,f2] |> [g1,g2]
let f1, g1 be morphism of C1; :: thesis: for f2, g2 being morphism of C2 st f1 |> g1 & f2 |> g2 holds
[f1,f2] |> [g1,g2]
let f2, g2 be morphism of C2; :: thesis: ( f1 |> g1 & f2 |> g2 implies [f1,f2] |> [g1,g2] )
assume A1: f1 |> g1 ; :: thesis: ( not f2 |> g2 or [f1,f2] |> [g1,g2] )
assume A2: f2 |> g2 ; :: thesis: [f1,f2] |> [g1,g2]
set G1 = COMPOSITION (f1,g1);
set G2 = COMPOSITION (f2,g2);
C1 [x] C2, pr1 (C1,C2), pr2 (C1,C2) is_product_of C1,C2 by Th48;
then consider H being Functor of (OrdC 3),(C1 [x] C2) such that
A3: ( H is covariant & (pr1 (C1,C2)) (*) H = COMPOSITION (f1,g1) & (pr2 (C1,C2)) (*) H = COMPOSITION (f2,g2) ) and
for H1 being Functor of (OrdC 3),(C1 [x] C2) st H1 is covariant & (pr1 (C1,C2)) (*) H1 = COMPOSITION (f1,g1) & (pr2 (C1,C2)) (*) H1 = COMPOSITION (f2,g2) holds
H = H1 by Def17;
consider g3, f3 being morphism of (OrdC 3) such that
A4: ( not g3 is identity & not f3 is identity & cod g3 = dom f3 ) and
Ob (OrdC 3) = {(dom g3),(cod g3),(cod f3)} and
Mor (OrdC 3) = {(dom g3),(cod g3),(cod f3),g3,f3,(f3 (*) g3)} and
dom g3, cod g3, cod f3,g3,f3,f3 (*) g3 are_mutually_distinct by Th18;
A5: f3 |> g3 by A4, CAT_7:5;
A6: (pr1 (C1,C2)) . (H . f3) = (COMPOSITION (f1,g1)) . f3 by A3, CAT_6:34
.= f1 by A1, A5, A4, Def1 ;
(pr2 (C1,C2)) . (H . f3) = (COMPOSITION (f2,g2)) . f3 by A3, CAT_6:34
.= f2 by A2, A5, A4, Def1 ;
then A7: H . f3 = [f1,f2] by A6, Def23;
A8: (pr1 (C1,C2)) . (H . g3) = (COMPOSITION (f1,g1)) . g3 by A3, CAT_6:34
.= g1 by A1, A5, A4, Def1 ;
(pr2 (C1,C2)) . (H . g3) = (COMPOSITION (f2,g2)) . g3 by A3, CAT_6:34
.= g2 by A2, A5, A4, Def1 ;
then A9: H . g3 = [g1,g2] by A8, Def23;
H is multiplicative by A3, CAT_6:def 25;
hence [f1,f2] |> [g1,g2] by A9, A7, A5, CAT_6:def 23; :: thesis: verum