now for o1, o2 being Object of C st not C is empty & ex f1 being morphism of C st
( o1 = f1 & f |> f1 & f1 is identity ) & ex f1 being morphism of C st
( o2 = f1 & f |> f1 & f1 is identity ) holds
o1 = o2let o1,
o2 be
Object of
C;
( not C is empty & ex f1 being morphism of C st
( o1 = f1 & f |> f1 & f1 is identity ) & ex f1 being morphism of C st
( o2 = f1 & f |> f1 & f1 is identity ) implies o1 = o2 )assume
not
C is
empty
;
( ex f1 being morphism of C st
( o1 = f1 & f |> f1 & f1 is identity ) & ex f1 being morphism of C st
( o2 = f1 & f |> f1 & f1 is identity ) implies o1 = o2 )assume
ex
f1 being
morphism of
C st
(
o1 = f1 &
f |> f1 &
f1 is
identity )
;
( ex f1 being morphism of C st
( o2 = f1 & f |> f1 & f1 is identity ) implies o1 = o2 )then consider f11 being
morphism of
C such that A3:
(
o1 = f11 &
f |> f11 &
f11 is
identity )
;
assume
ex
f1 being
morphism of
C st
(
o2 = f1 &
f |> f1 &
f1 is
identity )
;
o1 = o2then consider f12 being
morphism of
C such that A4:
(
o2 = f12 &
f |> f12 &
f12 is
identity )
;
(
f (*) f11 = f &
f (*) f12 = f )
by A3, A4, Def5;
then A5:
f11 |> f12
by A3, A4, Lm3;
f11 =
f11 (*) f12
by A5, A4, Def5
.=
f12
by A5, A3, Def4
;
hence
o1 = o2
by A3, A4;
verum end;
hence
for b1, b2 being Object of C holds
( ( not C is empty & ex f1 being morphism of C st
( b1 = f1 & f |> f1 & f1 is identity ) & ex f1 being morphism of C st
( b2 = f1 & f |> f1 & f1 is identity ) implies b1 = b2 ) & ( C is empty & b1 = the Object of C & b2 = the Object of C implies b1 = b2 ) )
; verum