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^> <> {} and

A4: ( <^o2,o3^> <> {} & <^o3,o2^> <> {} ) ; :: thesis: v = (f ") * u

thus (f ") * u = ((f ") * f) * v by A1, A3, A4, ALTCAT_1:21

.= v by A2, A3, ALTCAT_1:20 ; :: thesis: verum

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^> <> {} and

A4: ( <^o2,o3^> <> {} & <^o3,o2^> <> {} ) ; :: thesis: v = (f ") * u

thus (f ") * u = ((f ") * f) * v by A1, A3, A4, ALTCAT_1:21

.= v by A2, A3, ALTCAT_1:20 ; :: thesis: verum