let C1, C2 be 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] = [(f1 (*) g1),(f2 (*) 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] = [(f1 (*) g1),(f2 (*) g2)]
let f2, g2 be morphism of C2; :: thesis: ( f1 |> g1 & f2 |> g2 implies [f1,f2] (*) [g1,g2] = [(f1 (*) g1),(f2 (*) g2)] )
assume A1: f1 |> g1 ; :: thesis: ( not f2 |> g2 or [f1,f2] (*) [g1,g2] = [(f1 (*) g1),(f2 (*) g2)] )
then A2: not C1 is empty by CAT_6:1;
assume A3: f2 |> g2 ; :: thesis: [f1,f2] (*) [g1,g2] = [(f1 (*) g1),(f2 (*) g2)]
then A4: not C2 is empty by CAT_6:1;
A5: [f1,f2] |> [g1,g2] by A1, A3, Th54;
A6: (pr1 (C1,C2)) . ([f1,f2] (*) [g1,g2]) = ((pr1 (C1,C2)) . [f1,f2]) (*) ((pr1 (C1,C2)) . [g1,g2]) by A5, Th13
.= f1 (*) ((pr1 (C1,C2)) . [g1,g2]) by A2, A4, Def23
.= f1 (*) g1 by A2, A4, Def23 ;
(pr2 (C1,C2)) . ([f1,f2] (*) [g1,g2]) = ((pr2 (C1,C2)) . [f1,f2]) (*) ((pr2 (C1,C2)) . [g1,g2]) by A5, Th13
.= f2 (*) ((pr2 (C1,C2)) . [g1,g2]) by A2, A4, Def23
.= f2 (*) g2 by A2, A4, Def23 ;
hence [f1,f2] (*) [g1,g2] = [(f1 (*) g1),(f2 (*) g2)] by A2, A4, A6, Def23; :: thesis: verum