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 + H) = (J (#) G) + (J (#) H) )
let G, H, J be Functional_Sequence of D,REAL; :: thesis: ( (G + H) (#) J = (G (#) J) + (H (#) J) & J (#) (G + H) = (J (#) G) + (J (#) 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 Def5
.= ((G . n) (#) (J . n)) + ((H . n) (#) (J . n)) by RFUNCT_1:10
.= ((G (#) J) . n) + ((H . n) (#) (J . n)) by Def7
.= ((G (#) J) . n) + ((H (#) J) . n) by Def7
.= ((G (#) J) + (H (#) J)) . n by Def5 ; :: thesis: verum

end;

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