let C be Cocartesian_category; :: thesis: for a, b, c 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, b, c 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 :: thesis: ( g is epi implies 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 )
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, Th67;
then f1 * g = f2 * g by A7, A8, Th68;
hence f1 = f2 by A5, A6; :: thesis: verum
end;
A9: now :: thesis: ( f is epi implies 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 )
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, Th67;
then f1 * f = f2 * f by A12, A13, Th68;
hence f1 = f2 by A10, A11; :: thesis: verum
end;
Hom ((a + b),c) <> {} by A1, A2, Th65;
hence [$f,g$] is epi by A3, A9, A4; :: thesis: verum