let X be RealHilbertSpace; :: thesis: for f being linear-Functional of X st f is Lipschitzian holds

ex y being Point of X st

for x being Point of X holds f . x = x .|. y

let f be linear-Functional of X; :: thesis: ( f is Lipschitzian implies ex y being Point of X st

for x being Point of X holds f . x = x .|. y )

assume AS: f is Lipschitzian ; :: thesis: ex y being Point of X st

for x being Point of X holds f . x = x .|. y

set M = UKer f;

A1: the carrier of (UKer f) = f " {0} by defuker;

ex y being Point of X st

for x being Point of X holds f . x = x .|. y

let f be linear-Functional of X; :: thesis: ( f is Lipschitzian implies ex y being Point of X st

for x being Point of X holds f . x = x .|. y )

assume AS: f is Lipschitzian ; :: thesis: ex y being Point of X st

for x being Point of X holds f . x = x .|. y

set M = UKer f;

A1: the carrier of (UKer f) = f " {0} by defuker;

per cases
( the carrier of X = the carrier of (UKer f) or the carrier of X <> the carrier of (UKer f) )
;

end;

suppose AS1:
the carrier of X = the carrier of (UKer f)
; :: thesis: ex y being Point of X st

for x being Point of X holds f . x = x .|. y

for x being Point of X holds f . x = x .|. y

reconsider y = 0. X as Point of X ;

B1: for x being Point of X holds f . x = x .|. y

thus for x being Point of X holds f . x = x .|. y by B1; :: thesis: verum

end;B1: for x being Point of X holds f . x = x .|. y

proof

take
y
; :: thesis: for x being Point of X holds f . x = x .|. y
let x be Point of X; :: thesis: f . x = x .|. y

C11: ( x in X & f . x in {0} ) by FUNCT_2:38, AS1, A1;

x .|. y = 0 by BHSP_1:15;

hence f . x = x .|. y by C11, TARSKI:def 1; :: thesis: verum

end;C11: ( x in X & f . x in {0} ) by FUNCT_2:38, AS1, A1;

x .|. y = 0 by BHSP_1:15;

hence f . x = x .|. y by C11, TARSKI:def 1; :: thesis: verum

thus for x being Point of X holds f . x = x .|. y by B1; :: thesis: verum

suppose
the carrier of X <> the carrier of (UKer f)
; :: thesis: ex y being Point of X st

for x being Point of X holds f . x = x .|. y

for x being Point of X holds f . x = x .|. y

then
not the carrier of X c= the carrier of (UKer f)
by RUSUB_1:def 1;

then consider z being object such that

B1: ( z in the carrier of X & not z in the carrier of (UKer f) ) ;

reconsider y = z as Point of X by B1;

reconsider N = the carrier of (UKer f) as non empty Subset of X by A1;

consider y1, z1 being Point of X such that

C0: ( y1 in UKer f & z1 in Ort_Comp (UKer f) & y = y1 + z1 ) by Th87A, A1, AS, Lm89A;

C1: z1 <> 0. X by C0, B1;

then ||.z1.|| <> 0 by BHSP_1:26;

then C2: ||.z1.|| ^2 > 0 by SQUARE_1:12;

not z1 in UKer f by C0, C1, Lm89B;

then not z1 in f " {0} by defuker;

then not f . z1 in {0} by FUNCT_2:38;

then C3: f . z1 <> 0 by TARSKI:def 1;

set r = (f . z1) / (||.z1.|| ^2);

reconsider y = ((f . z1) / (||.z1.|| ^2)) * z1 as Point of X ;

C4: y in Ort_Comp (UKer f) by C0, RUSUB_1:15;

C5: for x being Point of X holds f . x = x .|. y

thus for x being Point of X holds f . x = x .|. y by C5; :: thesis: verum

end;then consider z being object such that

B1: ( z in the carrier of X & not z in the carrier of (UKer f) ) ;

reconsider y = z as Point of X by B1;

reconsider N = the carrier of (UKer f) as non empty Subset of X by A1;

consider y1, z1 being Point of X such that

C0: ( y1 in UKer f & z1 in Ort_Comp (UKer f) & y = y1 + z1 ) by Th87A, A1, AS, Lm89A;

C1: z1 <> 0. X by C0, B1;

then ||.z1.|| <> 0 by BHSP_1:26;

then C2: ||.z1.|| ^2 > 0 by SQUARE_1:12;

not z1 in UKer f by C0, C1, Lm89B;

then not z1 in f " {0} by defuker;

then not f . z1 in {0} by FUNCT_2:38;

then C3: f . z1 <> 0 by TARSKI:def 1;

set r = (f . z1) / (||.z1.|| ^2);

reconsider y = ((f . z1) / (||.z1.|| ^2)) * z1 as Point of X ;

C4: y in Ort_Comp (UKer f) by C0, RUSUB_1:15;

C5: for x being Point of X holds f . x = x .|. y

proof

take
y
; :: thesis: for x being Point of X holds f . x = x .|. y
let x be Point of X; :: thesis: f . x = x .|. y

set s = (f . x) / (f . z1);

reconsider y0 = x - (((f . x) / (f . z1)) * z1) as Point of X ;

D1: - (((f . x) / (f . z1)) * z1) = (- 1) * (((f . x) / (f . z1)) * z1) by RLVECT_1:16

.= ((- 1) * ((f . x) / (f . z1))) * z1 by RLVECT_1:def 7 ;

f . y0 = (f . x) + (f . (((- 1) * ((f . x) / (f . z1))) * z1)) by D1, HAHNBAN:def 2

.= (f . x) + (((- 1) * ((f . x) / (f . z1))) * (f . z1)) by HAHNBAN:def 3

.= (f . x) - (((f . x) / (f . z1)) * (f . z1))

.= (f . x) - (f . x) by C3, XCMPLX_1:87

.= 0 ;

then ( y0 in X & f . y0 in {0} ) by TARSKI:def 1;

then y0 in f " {0} by FUNCT_2:38;

then D2: y0 in UKer f by defuker;

y in { v where v is VECTOR of X : for w being VECTOR of X st w in UKer f holds

w,v are_orthogonal } by RUSUB_5:def 3, C4;

then consider v being VECTOR of X such that

D3: ( y = v & ( for w being VECTOR of X st w in UKer f holds

w,v are_orthogonal ) ) ;

D41: y0,y are_orthogonal by D2, D3;

D6: (x - (((f . x) / (f . z1)) * z1)) .|. (((f . z1) / (||.z1.|| ^2)) * z1) = (x .|. (((f . z1) / (||.z1.|| ^2)) * z1)) - ((((f . x) / (f . z1)) * z1) .|. (((f . z1) / (||.z1.|| ^2)) * z1)) by BHSP_1:11

.= (((f . z1) / (||.z1.|| ^2)) * (x .|. z1)) - ((((f . x) / (f . z1)) * z1) .|. (((f . z1) / (||.z1.|| ^2)) * z1)) by BHSP_1:3

.= (((f . z1) / (||.z1.|| ^2)) * (x .|. z1)) - (((f . x) / (f . z1)) * (z1 .|. (((f . z1) / (||.z1.|| ^2)) * z1))) by BHSP_1:def 2 ;

D7: ((f . x) / (f . z1)) * ((f . z1) / (||.z1.|| ^2)) = (f . x) / (||.z1.|| ^2) by C3, XCMPLX_1:98;

D8: 0 <= z1 .|. z1 by BHSP_1:def 2;

z1 .|. (((f . z1) / (||.z1.|| ^2)) * z1) = ((f . z1) / (||.z1.|| ^2)) * (z1 .|. z1) by BHSP_1:3

.= ((f . z1) / (||.z1.|| ^2)) * (||.z1.|| ^2) by D8, SQUARE_1:def 2 ;

then ((f . x) / (f . z1)) * (z1 .|. (((f . z1) / (||.z1.|| ^2)) * z1)) = ((f . x) / (||.z1.|| ^2)) * (||.z1.|| ^2) by D7

.= f . x by C2, XCMPLX_1:87 ;

hence f . x = x .|. y by BHSP_1:3, D6, D41; :: thesis: verum

end;set s = (f . x) / (f . z1);

reconsider y0 = x - (((f . x) / (f . z1)) * z1) as Point of X ;

D1: - (((f . x) / (f . z1)) * z1) = (- 1) * (((f . x) / (f . z1)) * z1) by RLVECT_1:16

.= ((- 1) * ((f . x) / (f . z1))) * z1 by RLVECT_1:def 7 ;

f . y0 = (f . x) + (f . (((- 1) * ((f . x) / (f . z1))) * z1)) by D1, HAHNBAN:def 2

.= (f . x) + (((- 1) * ((f . x) / (f . z1))) * (f . z1)) by HAHNBAN:def 3

.= (f . x) - (((f . x) / (f . z1)) * (f . z1))

.= (f . x) - (f . x) by C3, XCMPLX_1:87

.= 0 ;

then ( y0 in X & f . y0 in {0} ) by TARSKI:def 1;

then y0 in f " {0} by FUNCT_2:38;

then D2: y0 in UKer f by defuker;

y in { v where v is VECTOR of X : for w being VECTOR of X st w in UKer f holds

w,v are_orthogonal } by RUSUB_5:def 3, C4;

then consider v being VECTOR of X such that

D3: ( y = v & ( for w being VECTOR of X st w in UKer f holds

w,v are_orthogonal ) ) ;

D41: y0,y are_orthogonal by D2, D3;

D6: (x - (((f . x) / (f . z1)) * z1)) .|. (((f . z1) / (||.z1.|| ^2)) * z1) = (x .|. (((f . z1) / (||.z1.|| ^2)) * z1)) - ((((f . x) / (f . z1)) * z1) .|. (((f . z1) / (||.z1.|| ^2)) * z1)) by BHSP_1:11

.= (((f . z1) / (||.z1.|| ^2)) * (x .|. z1)) - ((((f . x) / (f . z1)) * z1) .|. (((f . z1) / (||.z1.|| ^2)) * z1)) by BHSP_1:3

.= (((f . z1) / (||.z1.|| ^2)) * (x .|. z1)) - (((f . x) / (f . z1)) * (z1 .|. (((f . z1) / (||.z1.|| ^2)) * z1))) by BHSP_1:def 2 ;

D7: ((f . x) / (f . z1)) * ((f . z1) / (||.z1.|| ^2)) = (f . x) / (||.z1.|| ^2) by C3, XCMPLX_1:98;

D8: 0 <= z1 .|. z1 by BHSP_1:def 2;

z1 .|. (((f . z1) / (||.z1.|| ^2)) * z1) = ((f . z1) / (||.z1.|| ^2)) * (z1 .|. z1) by BHSP_1:3

.= ((f . z1) / (||.z1.|| ^2)) * (||.z1.|| ^2) by D8, SQUARE_1:def 2 ;

then ((f . x) / (f . z1)) * (z1 .|. (((f . z1) / (||.z1.|| ^2)) * z1)) = ((f . x) / (||.z1.|| ^2)) * (||.z1.|| ^2) by D7

.= f . x by C2, XCMPLX_1:87 ;

hence f . x = x .|. y by BHSP_1:3, D6, D41; :: thesis: verum

thus for x being Point of X holds f . x = x .|. y by C5; :: thesis: verum