let V be non empty VectSpStr of 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 U2 of V #) = addLoopStr(# the carrier of (RealVS V),the addF of (RealVS V),the U2 of (RealVS V) #) by Def22;
hence p is Functional of (RealVS V) ; :: thesis: verum