let C be Cocartesian_category; :: thesis: for a, c, b being Object of C
for f being Morphism of a,c
for g being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} & ( f is epi or g is epi ) holds
[$f,g$] is epi
let a, c, b be Object of C; :: thesis: for f being Morphism of a,c
for g being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} & ( f is epi or g is epi ) holds
[$f,g$] is epi
let f be Morphism of a,c; :: thesis: for g being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} & ( f is epi or g is epi ) holds
[$f,g$] is epi
let g be Morphism of b,c; :: thesis: ( Hom (a,c) <> {} & Hom (b,c) <> {} & ( f is epi or g is epi ) implies [$f,g$] is epi )
assume that
A1: Hom (a,c) <> {} and
A2: Hom (b,c) <> {} and
A3: ( f is epi or g is epi ) ; :: thesis: [$f,g$] is epi

A4: now

assume A5: g is epi ; :: thesis: for d being Object of C
for f1, f2 being Morphism of c,d st Hom (c,d) <> {} & f1 * [$f,g$] = f2 * [$f,g$] holds
f1 = f2
let d be Object of C; :: thesis: for f1, f2 being Morphism of c,d st Hom (c,d) <> {} & f1 * [$f,g$] = f2 * [$f,g$] holds
f1 = f2
let f1, f2 be Morphism of c,d; :: thesis: ( Hom (c,d) <> {} & f1 * [$f,g$] = f2 * [$f,g$] implies f1 = f2 )
assume that
A6: Hom (c,d) <> {} and
A7: f1 * [$f,g$] = f2 * [$f,g$] ; :: thesis: f1 = f2
A8: ( Hom (a,d) <> {} & Hom (b,d) <> {} ) by A1, A2, A6, CAT_1:24;
( [$(f1 * f),(f1 * g)$] = f1 * [$f,g$] & [$(f2 * f),(f2 * g)$] = f2 * [$f,g$] ) by A1, A2, A6, Th72;
then f1 * g = f2 * g by A7, A8, Th73;
hence f1 = f2 by A2, A5, A6, CAT_1:36; :: thesis: verum

end;

A9: now

assume A10: f is epi ; :: thesis: for d being Object of C
for f1, f2 being Morphism of c,d st Hom (c,d) <> {} & f1 * [$f,g$] = f2 * [$f,g$] holds
f1 = f2
let d be Object of C; :: thesis: for f1, f2 being Morphism of c,d st Hom (c,d) <> {} & f1 * [$f,g$] = f2 * [$f,g$] holds
f1 = f2
let f1, f2 be Morphism of c,d; :: thesis: ( Hom (c,d) <> {} & f1 * [$f,g$] = f2 * [$f,g$] implies f1 = f2 )
assume that
A11: Hom (c,d) <> {} and
A12: f1 * [$f,g$] = f2 * [$f,g$] ; :: thesis: f1 = f2
A13: ( Hom (a,d) <> {} & Hom (b,d) <> {} ) by A1, A2, A11, CAT_1:24;
( [$(f1 * f),(f1 * g)$] = f1 * [$f,g$] & [$(f2 * f),(f2 * g)$] = f2 * [$f,g$] ) by A1, A2, A11, Th72;
then f1 * f = f2 * f by A12, A13, Th73;
hence f1 = f2 by A1, A10, A11, CAT_1:36; :: thesis: verum

end;

Hom ((a + b),c) <> {} by A1, A2, Th70;
hence [$f,g$] is epi by A3, A9, A4, CAT_1:36; :: thesis: verum