let V be non empty ModuleStr over INT.Ring ; :: thesis: for r being Element of F_Real
for f, g being FrFunctional of V holds r * (f + g) = (r * f) + (r * g)
let r be Element of F_Real; :: thesis: for f, g being FrFunctional of V holds r * (f + g) = (r * f) + (r * g)
let f, g be FrFunctional of V; :: thesis: r * (f + g) = (r * f) + (r * g)

now :: thesis: for x being Element of V holds (r * (f + g)) . x = ((r * f) + (r * g)) . x

let x be Element of V; :: thesis: (r * (f + g)) . x = ((r * f) + (r * g)) . x
thus (r * (f + g)) . x = r * ((f + g) . x) by HDef6
.= r * ((f . x) + (g . x)) by HDef3
.= (r * (f . x)) + (r * (g . x))
.= ((r * f) . x) + (r * (g . x)) by HDef6
.= ((r * f) . x) + ((r * g) . x) by HDef6
.= ((r * f) + (r * g)) . x by HDef3 ; :: thesis: verum

end;

hence r * (f + g) = (r * f) + (r * g) by FUNCT_2:63; :: thesis: verum