let C be Cocartesian_category; :: thesis: for a, c, b 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, c, b 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 Def29;
hence ( not [$f,g$] = [$k,h$] or ( f = k & g = h ) ) by A1, Def29; :: thesis: verum