let C1, C2 be category; 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; for f2, g2 being morphism of C2 holds
( [f1,f2] |> [g1,g2] iff ( f1 |> g1 & f2 |> g2 ) )
let f2, g2 be morphism of C2; ( [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 )
;
( [f1,f2] |> [g1,g2] iff ( f1 |> g1 & f2 |> g2 ) )hereby ( f1 |> g1 & f2 |> g2 implies [f1,f2] |> [g1,g2] )
assume A2:
[f1,f2] |> [g1,g2]
;
( 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;
f2 |> g2A4:
(
(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;
verum
end; assume
(
f1 |> g1 &
f2 |> g2 )
;
[f1,f2] |> [g1,g2]hence
[f1,f2] |> [g1,g2]
by A1, Lm2;
verum end; end;