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

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

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

end;

hence A1: (G - H) (#) J = (G (#) J) - (H (#) J) by FUNCT_2:63; :: thesis: (J (#) G) - (J (#) H) = J (#) (G - H)
thus (J (#) G) - (J (#) H) = (J (#) G) - (H (#) J) by Th5
.= (G - H) (#) J by A1, Th5
.= J (#) (G - H) by Th5 ; :: thesis: verum