let C be category; :: thesis: for o1, o2 being Object of (AllEpi C)

for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds

m is epi

let o1, o2 be Object of (AllEpi C); :: thesis: for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds

m is epi

let m be Morphism of o1,o2; :: thesis: ( <^o1,o2^> <> {} implies m is epi )

assume A1: <^o1,o2^> <> {} ; :: thesis: m is epi

reconsider p1 = o1, p2 = o2 as Object of C by Def2;

reconsider p = m as Morphism of p1,p2 by A1, ALTCAT_2:33;

p is epi by A1, Def2;

hence m is epi by A1, Th37; :: thesis: verum

for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds

m is epi

let o1, o2 be Object of (AllEpi C); :: thesis: for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds

m is epi

let m be Morphism of o1,o2; :: thesis: ( <^o1,o2^> <> {} implies m is epi )

assume A1: <^o1,o2^> <> {} ; :: thesis: m is epi

reconsider p1 = o1, p2 = o2 as Object of C by Def2;

reconsider p = m as Morphism of p1,p2 by A1, ALTCAT_2:33;

p is epi by A1, Def2;

hence m is epi by A1, Th37; :: thesis: verum