let D be non empty set ; :: thesis: for G, H, J being Functional_Sequence of D,REAL holds
( G (#) H = H (#) G & (G (#) H) (#) J = G (#) (H (#) J) )
let G, H, J be Functional_Sequence of D,REAL; :: thesis: ( G (#) H = H (#) G & (G (#) H) (#) J = G (#) (H (#) J) )

now :: thesis: for n being Element of NAT holds (G (#) H) . n = (H (#) G) . n

let n be Element of NAT ; :: thesis: (G (#) H) . n = (H (#) G) . n
thus (G (#) H) . n = (H . n) (#) (G . n) by Def7
.= (H (#) G) . n by Def7 ; :: thesis: verum

end;

hence G (#) H = H (#) G by FUNCT_2:63; :: thesis: (G (#) H) (#) J = G (#) (H (#) J)

now :: thesis: for n being Element of NAT holds ((G (#) H) (#) J) . n = (G (#) (H (#) J)) . n

let n be Element of NAT ; :: thesis: ((G (#) H) (#) J) . n = (G (#) (H (#) J)) . n
thus ((G (#) H) (#) J) . n = ((G (#) H) . n) (#) (J . n) by Def7
.= ((G . n) (#) (H . n)) (#) (J . n) by Def7
.= (G . n) (#) ((H . n) (#) (J . n)) by RFUNCT_1:9
.= (G . n) (#) ((H (#) J) . n) by Def7
.= (G (#) (H (#) J)) . n by Def7 ; :: thesis: verum

end;

hence (G (#) H) (#) J = G (#) (H (#) J) by FUNCT_2:63; :: thesis: verum