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

now :: thesis: for x being Element of V holds ((1. F_Real) * f) . x = f . x

let x be Element of V; :: thesis: ((1. F_Real) * f) . x = f . x
thus ((1. F_Real) * f) . x = (1. F_Real) * (f . x) by HDef6
.= f . x ; :: thesis: verum

end;

hence (1. F_Real) * f = f by FUNCT_2:63; :: thesis: verum