let C1, C2 be category; for f1 being morphism of C1
for f2 being morphism of C2
for f being morphism of (C1 [x] C2) st f = [f1,f2] & not C1 is empty & not C2 is empty holds
( f is identity iff ( f1 is identity & f2 is identity ) )
let f1 be morphism of C1; for f2 being morphism of C2
for f being morphism of (C1 [x] C2) st f = [f1,f2] & not C1 is empty & not C2 is empty holds
( f is identity iff ( f1 is identity & f2 is identity ) )
let f2 be morphism of C2; for f being morphism of (C1 [x] C2) st f = [f1,f2] & not C1 is empty & not C2 is empty holds
( f is identity iff ( f1 is identity & f2 is identity ) )
let f be morphism of (C1 [x] C2); ( f = [f1,f2] & not C1 is empty & not C2 is empty implies ( f is identity iff ( f1 is identity & f2 is identity ) ) )
assume A1:
f = [f1,f2]
; ( C1 is empty or C2 is empty or ( f is identity iff ( f1 is identity & f2 is identity ) ) )
assume A2:
( not C1 is empty & not C2 is empty )
; ( f is identity iff ( f1 is identity & f2 is identity ) )
assume A4:
( f1 is identity & f2 is identity )
; f is identity
for g being morphism of (C1 [x] C2) st f |> g holds
f (*) g = g
proof
let g be
morphism of
(C1 [x] C2);
( f |> g implies f (*) g = g )
assume A5:
f |> g
;
f (*) g = g
consider g1 being
morphism of
C1,
g2 being
morphism of
C2 such that A6:
g = [g1,g2]
by Th52;
A7:
(
f1 |> g1 &
f2 |> g2 )
by A6, A5, A1, Th54;
hence f (*) g =
[(f1 (*) g1),(f2 (*) g2)]
by A6, A1, Th55
.=
[g1,(f2 (*) g2)]
by A7, A4, Th4
.=
g
by A6, A7, A4, Th4
;
verum
end;
then A8:
f is left_identity
by CAT_6:def 4;
for g being morphism of (C1 [x] C2) st g |> f holds
g (*) f = g
proof
let g be
morphism of
(C1 [x] C2);
( g |> f implies g (*) f = g )
assume A9:
g |> f
;
g (*) f = g
consider g1 being
morphism of
C1,
g2 being
morphism of
C2 such that A10:
g = [g1,g2]
by Th52;
A11:
(
g1 |> f1 &
g2 |> f2 )
by A10, A9, A1, Th54;
hence g (*) f =
[(g1 (*) f1),(g2 (*) f2)]
by A10, A1, Th55
.=
[g1,(g2 (*) f2)]
by A11, A4, Th4
.=
g
by A10, A11, A4, Th4
;
verum
end;
hence
f is identity
by A8, CAT_6:def 5, CAT_6:def 14; verum