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

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