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:36; :: thesis: verum

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:36; :: thesis: verum