let X be RealUnitarySpace; :: thesis: ( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity implies for x being Point of X
for S being finite OrthonormalFamily of X st not S is empty holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) holds
setopfunc S,the carrier of X,REAL ,H,addreal <= ||.x.|| ^2 )
assume A1: ( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity ) ; :: thesis: for x being Point of X
for S being finite OrthonormalFamily of X st not S is empty holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) holds
setopfunc S,the carrier of X,REAL ,H,addreal <= ||.x.|| ^2
let x be Point of X; :: thesis: for S being finite OrthonormalFamily of X st not S is empty holds
for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) holds
setopfunc S,the carrier of X,REAL ,H,addreal <= ||.x.|| ^2
let S be finite OrthonormalFamily of X; :: thesis: ( not S is empty implies for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) holds
setopfunc S,the carrier of X,REAL ,H,addreal <= ||.x.|| ^2 )
assume A2: not S is empty ; :: thesis: for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) holds
setopfunc S,the carrier of X,REAL ,H,addreal <= ||.x.|| ^2
let H be Function of the carrier of X,REAL ; :: thesis: ( S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) implies setopfunc S,the carrier of X,REAL ,H,addreal <= ||.x.|| ^2 )
assume A3: ( S c= dom H & ( for y being Point of X st y in S holds
H . y = (x .|. y) ^2 ) ) ; :: thesis: setopfunc S,the carrier of X,REAL ,H,addreal <= ||.x.|| ^2

now

deffunc H₁( set ) -> set = the Mult of X . [(the scalar of X . [x,$1]),$1];
A4: for y being set st y in the carrier of X holds
H₁(y) in the carrier of X

proof

let y be set ; :: thesis: ( y in the carrier of X implies H₁(y) in the carrier of X )
assume A5: y in the carrier of X ; :: thesis: H₁(y) in the carrier of X
reconsider y1 = y as Point of X by A5;
set x1 = x;
the scalar of X . [x,y] = x .|. y1 by BHSP_1:def 1;
then reconsider a = the scalar of X . [x,y] as Real ;
reconsider y2 = y as VECTOR of X by A5;
the Mult of X . (the scalar of X . [x,y]),y = a * y2 ;
hence H₁(y) in the carrier of X ; :: thesis: verum

end;

ex F0 being Function of the carrier of X,the carrier of X st
for y being set st y in the carrier of X holds
F0 . y = H₁(y) from FUNCT_2:sch 2(A4);
then consider F0 being Function of the carrier of X,the carrier of X such that
A6: for y being set st y in the carrier of X holds
F0 . y = the Mult of X . [(the scalar of X . [x,y]),y] ;
A7: dom F0 = the carrier of X by FUNCT_2:def 1;

now

let y be Point of X; :: thesis: ( y in S implies F0 . y = (x .|. y) * y )
assume y in S ; :: thesis: F0 . y = (x .|. y) * y
thus F0 . y = the Mult of X . [(the scalar of X . [x,y]),y] by A6
.= (x .|. y) * y by BHSP_1:def 1 ; :: thesis: verum

end;

then consider F being Function of the carrier of X,the carrier of X such that
A8: ( S c= dom F & ( for y being Point of X st y in S holds
F . y = (x .|. y) * y ) ) by A7;
set z = setopfunc S,the carrier of X,the carrier of X,F,the addF of X;
(setopfunc S,the carrier of X,the carrier of X,F,the addF of X) .|. x = setopfunc S,the carrier of X,REAL ,H,addreal by A1, A2, A3, A8, Th11;
then x .|. (setopfunc S,the carrier of X,the carrier of X,F,the addF of X) = (setopfunc S,the carrier of X,the carrier of X,F,the addF of X) .|. (setopfunc S,the carrier of X,the carrier of X,F,the addF of X) by A1, A2, A3, A8, Th12;
then (x - (setopfunc S,the carrier of X,the carrier of X,F,the addF of X)) .|. (x - (setopfunc S,the carrier of X,the carrier of X,F,the addF of X)) = (((x .|. x) - ((setopfunc S,the carrier of X,the carrier of X,F,the addF of X) .|. (setopfunc S,the carrier of X,the carrier of X,F,the addF of X))) - ((setopfunc S,the carrier of X,the carrier of X,F,the addF of X) .|. (setopfunc S,the carrier of X,the carrier of X,F,the addF of X))) + ((setopfunc S,the carrier of X,the carrier of X,F,the addF of X) .|. (setopfunc S,the carrier of X,the carrier of X,F,the addF of X)) by BHSP_1:18
.= (x .|. x) - (setopfunc S,the carrier of X,REAL ,H,addreal ) by A1, A2, A3, A8, Th12 ;
hence 0 <= (x .|. x) - (setopfunc S,the carrier of X,REAL ,H,addreal ) by BHSP_1:def 2; :: thesis: verum

end;

then A9: 0 + (setopfunc S,the carrier of X,REAL ,H,addreal ) <= x .|. x by XREAL_1:21;
0 <= x .|. x by BHSP_1:def 2;
then setopfunc S,the carrier of X,REAL ,H,addreal <= (sqrt (x .|. x)) ^2 by A9, SQUARE_1:def 4;
hence setopfunc S,the carrier of X,REAL ,H,addreal <= ||.x.|| ^2 by BHSP_1:def 4; :: thesis: verum