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