set C = the carrier of V;

defpred S_{1}[ Element of the carrier of V, set ] means $2 = sqrt (signnorm (f,$1));

A2: for v being Element of V holds S_{1}[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

defpred S

A1: now :: thesis: for x being Element of the carrier of V ex y being Element of REAL st S_{1}[x,y]

consider F being Function of the carrier of V,REAL such that let x be Element of the carrier of V; :: thesis: ex y being Element of REAL st S_{1}[x,y]

reconsider y = sqrt (signnorm (f,x)) as Element of REAL by XREAL_0:def 1;

take y = y; :: thesis: S_{1}[x,y]

thus S_{1}[x,y]
; :: thesis: verum

end;reconsider y = sqrt (signnorm (f,x)) as Element of REAL by XREAL_0:def 1;

take y = y; :: thesis: S

thus S

A2: for v being Element of V holds S

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