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: 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
A6: Hom c,d <> {} and
A7: f1 * [$f,g$] = f2 * [$f,g$] ; :: thesis: f1 = f2
( [$(f1 * f),(f1 * g)$] = f1 * [$f,g$] & [$(f2 * f),(f2 * g)$] = f2 * [$f,g$] & Hom a,d <> {} & Hom b,d <> {} ) by A1, A2, A6, Th72, CAT_1:52;
then f1 * f = f2 * f by A7, Th73;
hence f1 = f2 by A1, A5, A6, CAT_1:65; :: thesis: verum

end;

A8: Hom (a + b),c <> {} by A1, A2, Th70;

now

assume A9: 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
A10: Hom c,d <> {} and
A11: f1 * [$f,g$] = f2 * [$f,g$] ; :: thesis: f1 = f2
( [$(f1 * f),(f1 * g)$] = f1 * [$f,g$] & [$(f2 * f),(f2 * g)$] = f2 * [$f,g$] & Hom a,d <> {} & Hom b,d <> {} ) by A1, A2, A10, Th72, CAT_1:52;
then f1 * g = f2 * g by A11, Th73;
hence f1 = f2 by A2, A9, A10, CAT_1:65; :: thesis: verum

end;

hence [$f,g$] is epi by A3, A4, A8, CAT_1:65; :: thesis: verum