set C = the carrier of V;
defpred S₁[ Element of the carrier of V, set ] means $2 = sqrt (signnorm (f,$1));

A1: now :: thesis: for x being Element of the carrier of V ex y being Element of REAL st S₁[x,y]

let x be Element of the carrier of V; :: thesis: ex y being Element of REAL st S₁[x,y]
reconsider y = sqrt (signnorm (f,x)) as Element of REAL by XREAL_0:def 1;
take y = y; :: thesis: S₁[x,y]
thus S₁[x,y] ; :: thesis: verum

end;

consider F being Function of the carrier of V,REAL such that
A2: for v being Element of V holds S₁[v,F . v] from FUNCT_2:sch 3(A1);
reconsider F = F as RFunctional of V ;
take F ; :: thesis: for v being Element of V holds F . v = sqrt (signnorm (f,v))
thus for v being Element of V holds F . v = sqrt (signnorm (f,v)) by A2; :: thesis: verum