let C be Cartesian_category; :: thesis: for a, b, c 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 a, b, c 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 :: thesis: ( g is monic implies 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 )
assume A5: 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
A6: Hom (d,c) <> {} and
A7: <:f,g:> * f1 = <:f,g:> * f2 ; :: thesis: f1 = f2
A8: ( Hom (d,a) <> {} & Hom (d,b) <> {} ) by A1, A2, A6, CAT_1:24;
( <:(f * f1),(g * f1):> = <:f,g:> * f1 & <:(f * f2),(g * f2):> = <:f,g:> * f2 ) by A1, A2, A6, Th25;
then g * f1 = g * f2 by A7, A8, Th26;
hence f1 = f2 by A5, A6; :: thesis: verum
end;
A9: now :: thesis: ( f is monic implies 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 )
assume A10: 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
A11: Hom (d,c) <> {} and
A12: <:f,g:> * f1 = <:f,g:> * f2 ; :: thesis: f1 = f2
A13: ( Hom (d,a) <> {} & Hom (d,b) <> {} ) by A1, A2, A11, CAT_1:24;
( <:(f * f1),(g * f1):> = <:f,g:> * f1 & <:(f * f2),(g * f2):> = <:f,g:> * f2 ) by A1, A2, A11, Th25;
then f * f1 = f * f2 by A12, A13, Th26;
hence f1 = f2 by A10, A11; :: thesis: verum
end;
Hom (c,(a [x] b)) <> {} by A1, A2, Th23;
hence <:f,g:> is monic by A3, A9, A4; :: thesis: verum