let V be non empty ModuleStr over F_Complex ; :: thesis: for p being RFunctional of V holds p is Functional of (RealVS V)
let p be RFunctional of V; :: thesis: p is Functional of (RealVS V)
addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
hence p is Functional of (RealVS V) ; :: thesis: verum