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 that
A1: ( the addF of X is commutative & the addF of X is associative ) and
A2: 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 A3: 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 that
A4: S c= dom H and
A5: 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 :: thesis: 0 <= (x .|. x) - (setopfunc (S, the carrier of X,REAL,H,addreal))

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

proof

let y be object ; :: thesis: ( y in the carrier of X implies H₁(y) in the carrier of X )
assume A7: y in the carrier of X ; :: thesis: H₁(y) in the carrier of X
reconsider y1 = y as Point of X by A7;
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 A7;
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 object st y in the carrier of X holds
F0 . y = H₁(y) from FUNCT_2:sch 2(A6);
then consider F0 being Function of the carrier of X, the carrier of X such that
A8: for y being object st y in the carrier of X holds
F0 . y = the Mult of X . [( the scalar of X . [x,y]),y] ;
A9: dom F0 = the carrier of X by FUNCT_2:def 1;

now :: thesis: for y being Point of X st y in S holds
F0 . y = (x .|. y) * y

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 A8
.= (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
A10: S c= dom F and
A11: for y being Point of X st y in S holds
F . y = (x .|. y) * y by A9;
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, A4, A5, A10, A11, 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, A4, A5, A10, A11, 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:13
.= (x .|. x) - (setopfunc (S, the carrier of X,REAL,H,addreal)) by A1, A2, A3, A4, A5, A10, A11, Th12 ;
hence 0 <= (x .|. x) - (setopfunc (S, the carrier of X,REAL,H,addreal)) by BHSP_1:def 2; :: thesis: verum

end;

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