let C be category; :: thesis: for o1, o2 being object of
for f being Morphism of ,
for g, h being Morphism of , st h * f = idm o1 & f * g = idm o2 & <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
g = h
let o1, o2 be object of ; :: thesis: for f being Morphism of ,
for g, h being Morphism of , st h * f = idm o1 & f * g = idm o2 & <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
g = h
let f be Morphism of ,; :: thesis: for g, h being Morphism of , st h * f = idm o1 & f * g = idm o2 & <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
g = h
let g, h be Morphism of ,; :: 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:24
.= h * (idm o2) by A2, A3, ALTCAT_1:25
.= h by A3, ALTCAT_1:def 19 ; :: thesis: verum