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 A1: ( <^a,b^> <> {} & <^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, ALTCAT_1:def 4;
hence g * f = g * f by A1, ALTCAT_1:def 14; :: thesis: verum