let C be non empty AltCatStr ; :: thesis: 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; :: thesis: for M being Morphism of A,O st O is initial holds
M is epi
let M be Morphism of A,O; :: thesis: ( O is initial implies M is epi )
assume A1: O is initial ; :: thesis: M is epi
let o be object of C; :: according to ALTCAT_3:def 8 :: thesis: ( <^O,o^> = {} or for b₁, b₂ being M2(<^O,o^>) holds
( not b₁ * M = b₂ * M or b₁ = b₂ ) )
assume A2: <^O,o^> <> {} ; :: thesis: for b₁, b₂ being M2(<^O,o^>) holds
( not b₁ * M = b₂ * M or b₁ = b₂ )
let a, b be Morphism of O,o; :: thesis: ( not a * M = b * M or a = b )
assume a * M = b * M ; :: thesis: 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 ; :: thesis: verum