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 ( Hom a,c <> {} & Hom b,c <> {} ) ; :: thesis: ( not [$f,g$] = [$k,h$] or ( f = k & g = h ) )
then ( [$f,g$] * (in1 a,b) = f & [$k,h$] * (in1 a,b) = k & [$f,g$] * (in2 a,b) = g & [$k,h$] * (in2 a,b) = h ) by Def29;
hence ( not [$f,g$] = [$k,h$] or ( f = k & g = h ) ) ; :: thesis: verum