let C be Cocartesian_category; 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; 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; 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; ( 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 )
; [$f,g$] is epi
A4:
now ( 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
;
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 = f2let d be
Object of
C;
for f1, f2 being Morphism of c,d st Hom (c,d) <> {} & f1 * [$f,g$] = f2 * [$f,g$] holds
f1 = f2let f1,
f2 be
Morphism of
c,
d;
( 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$]
;
f1 = f2A8:
(
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;
verum end;
A9:
now ( 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
;
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 = f2let d be
Object of
C;
for f1, f2 being Morphism of c,d st Hom (c,d) <> {} & f1 * [$f,g$] = f2 * [$f,g$] holds
f1 = f2let f1,
f2 be
Morphism of
c,
d;
( 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$]
;
f1 = f2A13:
(
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;
verum end;
Hom ((a + b),c) <> {}
by A1, A2, Th65;
hence
[$f,g$] is epi
by A3, A9, A4; verum