let C be category; :: thesis: for o1, o2 being object of
for m being Morphism of , st <^o1,o2^> <> {} holds
m is epi
let o1, o2 be object of ; :: thesis: for m being Morphism of , st <^o1,o2^> <> {} holds
m is epi
let m be Morphism of ,; :: thesis: ( <^o1,o2^> <> {} implies m is epi )
assume A1: <^o1,o2^> <> {} ; :: thesis: m is epi
reconsider p1 = o1, p2 = o2 as object of by Def2;
reconsider p = m as Morphism of , by A1, ALTCAT_2:34;
p is epi by A1, Def2;
hence m is epi by A1, Th37; :: thesis: verum