let C be Cartesian_category; :: thesis: for c, a, b being Object of C
for f, k being Morphism of c,a
for g, h being Morphism of c,b st Hom c,a <> {} & Hom c,b <> {} & <:f,g:> = <:k,h:> holds
( f = k & g = h )
let c, a, b be Object of C; :: thesis: for f, k being Morphism of c,a
for g, h being Morphism of c,b st Hom c,a <> {} & Hom c,b <> {} & <:f,g:> = <:k,h:> holds
( f = k & g = h )
let f, k be Morphism of c,a; :: thesis: for g, h being Morphism of c,b st Hom c,a <> {} & Hom c,b <> {} & <:f,g:> = <:k,h:> holds
( f = k & g = h )
let g, h be Morphism of c,b; :: thesis: ( Hom c,a <> {} & Hom c,b <> {} & <:f,g:> = <:k,h:> implies ( f = k & g = h ) )
assume ( Hom c,a <> {} & Hom c,b <> {} ) ; :: thesis: ( not <:f,g:> = <:k,h:> or ( f = k & g = h ) )
then ( (pr1 a,b) * <:f,g:> = f & (pr1 a,b) * <:k,h:> = k & (pr2 a,b) * <:f,g:> = g & (pr2 a,b) * <:k,h:> = h ) by Def11;
hence ( not <:f,g:> = <:k,h:> or ( f = k & g = h ) ) ; :: thesis: verum