let C be semi-functional para-functional category; :: thesis: for a, b, c being Object of C st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = g * f
let a, b, c be Object of C; :: thesis: ( <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b
for g being Morphism of b,c holds g * f = g * f )
assume that
A1: <^a,b^> <> {} and
A2: <^b,c^> <> {} ; :: thesis: for f being Morphism of a,b
for g being Morphism of b,c holds g * f = g * f
let f be Morphism of a,b; :: thesis: for g being Morphism of b,c holds g * f = g * f
let g be Morphism of b,c; :: thesis: g * f = g * f
<^a,c^> <> {} by A1, A2, ALTCAT_1:def 2;
hence g * f = g * f by A1, A2, ALTCAT_1:def 12; :: thesis: verum