let C1, C2 be category; :: thesis: for f1, g1 being morphism of C1
for f2, g2 being morphism of C2 holds
( [f1,f2] |> [g1,g2] iff ( f1 |> g1 & f2 |> g2 ) )
let f1, g1 be morphism of C1; :: thesis: for f2, g2 being morphism of C2 holds
( [f1,f2] |> [g1,g2] iff ( f1 |> g1 & f2 |> g2 ) )
let f2, g2 be morphism of C2; :: thesis: ( [f1,f2] |> [g1,g2] iff ( f1 |> g1 & f2 |> g2 ) )

per cases ( ( not C1 is empty & not C2 is empty ) or C1 is empty or C2 is empty ) ;

suppose A1: ( not C1 is empty & not C2 is empty ) ; :: thesis: ( [f1,f2] |> [g1,g2] iff ( f1 |> g1 & f2 |> g2 ) )

hereby :: thesis: ( f1 |> g1 & f2 |> g2 implies [f1,f2] |> [g1,g2] )

assume A2: [f1,f2] |> [g1,g2] ; :: thesis: ( f1 |> g1 & f2 |> g2 )
A3: ( (pr1 (C1,C2)) . [f1,f2] = f1 & (pr1 (C1,C2)) . [g1,g2] = g1 ) by A1, Def23;
pr1 (C1,C2) is multiplicative by CAT_6:def 25;
hence f1 |> g1 by A3, A2, CAT_6:def 23; :: thesis: f2 |> g2
A4: ( (pr2 (C1,C2)) . [f1,f2] = f2 & (pr2 (C1,C2)) . [g1,g2] = g2 ) by A1, Def23;
pr2 (C1,C2) is multiplicative by CAT_6:def 25;
hence f2 |> g2 by A4, A2, CAT_6:def 23; :: thesis: verum

end;

assume ( f1 |> g1 & f2 |> g2 ) ; :: thesis: [f1,f2] |> [g1,g2]
hence [f1,f2] |> [g1,g2] by A1, Lm2; :: thesis: verum

end;

suppose ( C1 is empty or C2 is empty ) ; :: thesis: ( [f1,f2] |> [g1,g2] iff ( f1 |> g1 & f2 |> g2 ) )

hence ( [f1,f2] |> [g1,g2] iff ( f1 |> g1 & f2 |> g2 ) ) by CAT_6:1; :: thesis: verum

end;

end;