let C be lattice-wise category; 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; ( <^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^> <> {} )
; 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; for g being Morphism of b,c holds g * f = (@ g) * (@ f)
let g be Morphism of b,c; g * f = (@ g) * (@ f)
( f = @ f & g = @ g )
by A1, Def7;
hence
g * f = (@ g) * (@ f)
by A1, YELLOW18:36; verum