let C be category; :: thesis: for o1, o2, o3 being object of C
for v being Morphism of o1,o2
for u being Morphism of o1,o3
for f being Morphism of o2,o3 st u = f * v & (f " ) * f = idm o2 & <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o2^> <> {} holds
v = (f " ) * u
let o1, o2, o3 be object of C; :: thesis: for v being Morphism of o1,o2
for u being Morphism of o1,o3
for f being Morphism of o2,o3 st u = f * v & (f " ) * f = idm o2 & <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o2^> <> {} holds
v = (f " ) * u
let v be Morphism of o1,o2; :: thesis: for u being Morphism of o1,o3
for f being Morphism of o2,o3 st u = f * v & (f " ) * f = idm o2 & <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o2^> <> {} holds
v = (f " ) * u
let u be Morphism of o1,o3; :: thesis: for f being Morphism of o2,o3 st u = f * v & (f " ) * f = idm o2 & <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o2^> <> {} holds
v = (f " ) * u
let f be Morphism of o2,o3; :: thesis: ( u = f * v & (f " ) * f = idm o2 & <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o2^> <> {} implies v = (f " ) * u )
assume that
A1: u = f * v and
A2: (f " ) * f = idm o2 and
A3: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o2^> <> {} ) ; :: thesis: v = (f " ) * u
thus (f " ) * u = ((f " ) * f) * v by A1, A3, ALTCAT_1:25
.= v by A2, A3, ALTCAT_1:24 ; :: thesis: verum