let C be lattice-wise 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)
( f = @ f & g = @ g ) by A1, Def7;
hence g * f = (@ g) * (@ f) by A1, YELLOW18:38; :: thesis: verum