let C be Cartesian_category; :: thesis: for a, b, c 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 a, b, c 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 A1: ( Hom (c,a) <> {} & Hom (c,b) <> {} ) ; :: thesis: ( not <:f,g:> = <:k,h:> or ( f = k & g = h ) )
then ( (pr1 (a,b)) * <:f,g:> = f & (pr2 (a,b)) * <:f,g:> = g ) by Def10;
hence ( not <:f,g:> = <:k,h:> or ( f = k & g = h ) ) by A1, Def10; :: thesis: verum