let C be Cocartesian_category; :: thesis: for a, b, c being Object of C
for f, k being Morphism of a,c
for g, h being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} & [$f,g$] = [$k,h$] holds
( f = k & g = h )
let a, b, c be Object of C; :: thesis: for f, k being Morphism of a,c
for g, h being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} & [$f,g$] = [$k,h$] holds
( f = k & g = h )
let f, k be Morphism of a,c; :: thesis: for g, h being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} & [$f,g$] = [$k,h$] holds
( f = k & g = h )
let g, h be Morphism of b,c; :: thesis: ( Hom (a,c) <> {} & Hom (b,c) <> {} & [$f,g$] = [$k,h$] implies ( f = k & g = h ) )
assume A1: ( Hom (a,c) <> {} & Hom (b,c) <> {} ) ; :: thesis: ( not [$f,g$] = [$k,h$] or ( f = k & g = h ) )
then ( [$f,g$] * (in1 (a,b)) = f & [$f,g$] * (in2 (a,b)) = g ) by Def28;
hence ( not [$f,g$] = [$k,h$] or ( f = k & g = h ) ) by A1, Def28; :: thesis: verum