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_{1}, b_{2} being M3(<^O,o^>) holds

( not b_{1} * M = b_{2} * M or b_{1} = b_{2} ) )

assume A2: <^O,o^> <> {} ; :: thesis: for b_{1}, b_{2} being M3(<^O,o^>) holds

( not b_{1} * M = b_{2} * M or b_{1} = b_{2} )

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

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

( not b

assume A2: <^O,o^> <> {} ; :: thesis: for b

( not 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