let f, g be Function of X,T; :: thesis: f (#) g = g (#) f
let x be Element of X; :: according to FUNCT_2:def 8 :: thesis: (f (#) g) . x = (g (#) f) . x
thus (f (#) g) . x = (f . x) * (g . x) by Def2
.= (g (#) f) . x by Def2 ; :: thesis: verum