let C be non empty AltCatStr ; for O, A being Object of C
for M being Morphism of A,O st O is initial holds
M is epi
let O, A be Object of C; for M being Morphism of A,O st O is initial holds
M is epi
let M be Morphism of A,O; ( O is initial implies M is epi )
assume A1:
O is initial
; M is epi
let o be Object of C; ALTCAT_3:def 8 ( <^O,o^> = {} or for b1, b2 being M3(<^O,o^>) holds
( not b1 * M = b2 * M or b1 = b2 ) )
assume A2:
<^O,o^> <> {}
; for b1, b2 being M3(<^O,o^>) holds
( not b1 * M = b2 * M or b1 = b2 )
let a, b be Morphism of O,o; ( not a * M = b * M or a = b )
assume
a * M = b * M
; a = b
consider N being Morphism of O,o such that
N in <^O,o^>
and
A3:
for M1 being Morphism of O,o st M1 in <^O,o^> holds
N = M1
by A1, ALTCAT_3:25;
thus a =
N
by A2, A3
.=
b
by A2, A3
; verum