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

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

let n be Element of NAT ; :: thesis: (r (#) (G + H)) . n = ((r (#) G) + (r (#) H)) . n
thus (r (#) (G + H)) . n = r (#) ((G + H) . n) by Def1
.= r (#) ((G . n) + (H . n)) by Def5
.= (r (#) (G . n)) + (r (#) (H . n)) by RFUNCT_1:16
.= ((r (#) G) . n) + (r (#) (H . n)) by Def1
.= ((r (#) G) . n) + ((r (#) H) . n) by Def1
.= ((r (#) G) + (r (#) H)) . n by Def5 ; :: thesis: verum

end;

hence r (#) (G + H) = (r (#) G) + (r (#) H) by FUNCT_2:63; :: thesis: r (#) (G - H) = (r (#) G) - (r (#) H)

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

let n be Element of NAT ; :: thesis: (r (#) (G - H)) . n = ((r (#) G) - (r (#) H)) . n
thus (r (#) (G - H)) . n = r (#) ((G - H) . n) by Def1
.= r (#) ((G . n) - (H . n)) by Th3
.= (r (#) (G . n)) - (r (#) (H . n)) by RFUNCT_1:18
.= ((r (#) G) . n) - (r (#) (H . n)) by Def1
.= ((r (#) G) . n) - ((r (#) H) . n) by Def1
.= ((r (#) G) - (r (#) H)) . n by Th3 ; :: thesis: verum

end;

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