let C1, C2 be with_identities CategoryStr ; ( CategoryStr(# the carrier of C1, the composition of C1 #) = CategoryStr(# the carrier of C2, the composition of C2 #) implies for f1 being morphism of C1
for f2 being morphism of C2 st f1 = f2 holds
( f1 is identity iff f2 is identity ) )
assume A1:
CategoryStr(# the carrier of C1, the composition of C1 #) = CategoryStr(# the carrier of C2, the composition of C2 #)
; for f1 being morphism of C1
for f2 being morphism of C2 st f1 = f2 holds
( f1 is identity iff f2 is identity )
let f1 be morphism of C1; for f2 being morphism of C2 st f1 = f2 holds
( f1 is identity iff f2 is identity )
let f2 be morphism of C2; ( f1 = f2 implies ( f1 is identity iff f2 is identity ) )
assume A2:
f1 = f2
; ( f1 is identity iff f2 is identity )
hereby ( f2 is identity implies f1 is identity )
assume A3:
f1 is
identity
;
f2 is identity A4:
for
f being
morphism of
C2 st
f2 |> f holds
f2 (*) f = f
proof
let f be
morphism of
C2;
( f2 |> f implies f2 (*) f = f )
assume A5:
f2 |> f
;
f2 (*) f = f
reconsider f3 =
f as
morphism of
C1 by A1;
thus f2 (*) f =
the
composition of
C2 . (
f2,
f)
by A5, Def3
.=
f1 (*) f3
by A5, A2, A1, Def3, Def2
.=
f
by A5, A3, Def4, Def2, A1, A2
;
verum
end;
for
f being
morphism of
C2 st
f,
f2 are_composable holds
f (*) f2 = f
proof
let f be
morphism of
C2;
( f,f2 are_composable implies f (*) f2 = f )
assume A6:
f |> f2
;
f (*) f2 = f
reconsider f3 =
f as
morphism of
C1 by A1;
thus f (*) f2 =
the
composition of
C2 . (
f,
f2)
by A6, Def3
.=
f3 (*) f1
by A6, A2, A1, Def3, Def2
.=
f
by A6, A3, Def5, Def2, A1, A2
;
verum
end; then
f2 is
right_identity
;
hence
f2 is
identity
by A4, Def4;
verum
end;
assume A7:
f2 is identity
; f1 is identity
A8:
for f being morphism of C1 st f1 |> f holds
f1 (*) f = f
proof
let f be
morphism of
C1;
( f1 |> f implies f1 (*) f = f )
assume A9:
f1 |> f
;
f1 (*) f = f
reconsider f3 =
f as
morphism of
C2 by A1;
thus f1 (*) f =
the
composition of
C1 . (
f1,
f)
by A9, Def3
.=
f2 (*) f3
by A9, A2, A1, Def3, Def2
.=
f
by A9, A7, Def4, Def2, A1, A2
;
verum
end;
for f being morphism of C1 st f |> f1 holds
f (*) f1 = f
proof
let f be
morphism of
C1;
( f |> f1 implies f (*) f1 = f )
assume A10:
f |> f1
;
f (*) f1 = f
reconsider f3 =
f as
morphism of
C2 by A1;
thus f (*) f1 =
the
composition of
C1 . (
f,
f1)
by A10, Def3
.=
f3 (*) f2
by A10, A2, A1, Def3, Def2
.=
f
by A10, A7, Def5, Def2, A1, A2
;
verum
end;
then
f1 is right_identity
;
hence
f1 is identity
by A8, Def4; verum