let C be Category; :: thesis: for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} & Hom (b,a) <> {} holds
for g1, g2 being Morphism of b,a st f * g1 = id b & g2 * f = id a holds
g1 = g2
let a, b be Object of C; :: thesis: for f being Morphism of a,b st Hom (a,b) <> {} & Hom (b,a) <> {} holds
for g1, g2 being Morphism of b,a st f * g1 = id b & g2 * f = id a holds
g1 = g2
let f be Morphism of a,b; :: thesis: ( Hom (a,b) <> {} & Hom (b,a) <> {} implies for g1, g2 being Morphism of b,a st f * g1 = id b & g2 * f = id a holds
g1 = g2 )
assume that
A1: Hom (a,b) <> {} and
A2: Hom (b,a) <> {} ; :: thesis: for g1, g2 being Morphism of b,a st f * g1 = id b & g2 * f = id a holds
g1 = g2
let g1, g2 be Morphism of b,a; :: thesis: ( f * g1 = id b & g2 * f = id a implies g1 = g2 )
assume A3: f * g1 = id b ; :: thesis: ( not g2 * f = id a or g1 = g2 )
assume g2 * f = id a ; :: thesis: g1 = g2
hence g1 = (g2 * f) * g1 by A2, Th23
.= g2 * (id b) by A1, A2, A3, Th21
.= g2 by A2, Th24 ;
:: thesis: verum