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

A4: now

assume A5: f is monic ; :: thesis: for d being Object of C
for f1, f2 being Morphism of d,c st Hom d,c <> {} & <:f,g:> * f1 = <:f,g:> * f2 holds
f1 = f2
let d be Object of C; :: thesis: for f1, f2 being Morphism of d,c st Hom d,c <> {} & <:f,g:> * f1 = <:f,g:> * f2 holds
f1 = f2
let f1, f2 be Morphism of d,c; :: thesis: ( Hom d,c <> {} & <:f,g:> * f1 = <:f,g:> * f2 implies f1 = f2 )
assume that
A6: Hom d,c <> {} and
A7: <:f,g:> * f1 = <:f,g:> * f2 ; :: thesis: f1 = f2
( <:(f * f1),(g * f1):> = <:f,g:> * f1 & <:(f * f2),(g * f2):> = <:f,g:> * f2 & Hom d,a <> {} & Hom d,b <> {} ) by A1, A2, A6, Th27, CAT_1:52;
then f * f1 = f * f2 by A7, Th28;
hence f1 = f2 by A1, A5, A6, CAT_1:60; :: thesis: verum

end;

A8: Hom c,(a [x] b) <> {} by A1, A2, Th25;

now

assume A9: g is monic ; :: thesis: for d being Object of C
for f1, f2 being Morphism of d,c st Hom d,c <> {} & <:f,g:> * f1 = <:f,g:> * f2 holds
f1 = f2
let d be Object of C; :: thesis: for f1, f2 being Morphism of d,c st Hom d,c <> {} & <:f,g:> * f1 = <:f,g:> * f2 holds
f1 = f2
let f1, f2 be Morphism of d,c; :: thesis: ( Hom d,c <> {} & <:f,g:> * f1 = <:f,g:> * f2 implies f1 = f2 )
assume that
A10: Hom d,c <> {} and
A11: <:f,g:> * f1 = <:f,g:> * f2 ; :: thesis: f1 = f2
( <:(f * f1),(g * f1):> = <:f,g:> * f1 & <:(f * f2),(g * f2):> = <:f,g:> * f2 & Hom d,a <> {} & Hom d,b <> {} ) by A1, A2, A10, Th27, CAT_1:52;
then g * f1 = g * f2 by A11, Th28;
hence f1 = f2 by A2, A9, A10, CAT_1:60; :: thesis: verum

end;

hence <:f,g:> is monic by A3, A4, A8, CAT_1:60; :: thesis: verum