let C be category; :: thesis: for o1, o2 being Object of C
for f being Morphism of o1,o2
for g, h being Morphism of o2,o1 st h * f = idm o1 & f * g = idm o2 & <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
g = h
let o1, o2 be Object of C; :: thesis: for f being Morphism of o1,o2
for g, h being Morphism of o2,o1 st h * f = idm o1 & f * g = idm o2 & <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
g = h
let f be Morphism of o1,o2; :: thesis: for g, h being Morphism of o2,o1 st h * f = idm o1 & f * g = idm o2 & <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
g = h
let g, h be Morphism of o2,o1; :: thesis: ( h * f = idm o1 & f * g = idm o2 & <^o1,o2^> <> {} & <^o2,o1^> <> {} implies g = h )
assume that
A1: h * f = idm o1 and
A2: ( f * g = idm o2 & <^o1,o2^> <> {} ) and
A3: <^o2,o1^> <> {} ; :: thesis: g = h
thus g = (h * f) * g by A1, A3, ALTCAT_1:20
.= h * (idm o2) by A2, A3, ALTCAT_1:21
.= h by A3, ALTCAT_1:def 17 ; :: thesis: verum