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