= k & m >= k holds |. (SA.m + SB.n) - 4*(d*d) .| < e proof let e be Real; assume B01: 0 < e; then consider k1 be Nat such that B1: for n be Nat st n >= k1 holds |.SA.n - 2*(d*d).| < e/2 by A5,C5,SEQ_2:def 7; consider k2 be Nat such that B2: for m be Nat st m >= k2 holds |.SB.m - 2*(d*d).| < e/2 by B01,A5,C6,SEQ_2:def 7; max(k1,k2) is natural; then reconsider k=max(k1,k2) as Nat; B3: for n,m be Nat st n >= k & m >= k holds |.(SA.m + SB.n) - 4*(d*d).| < e proof let n,m be Nat; assume AS: n >= k & m >= k; k >= k1 & k >= k2 by XXREAL_0:25; then C0: n >= k1 & m >= k2 by AS,XXREAL_0:2; then C1: |.SA.n - 2*(d*d).| < e/2 by B1; C2: |.SB.m - 2*(d*d).| < e/2 by C0,B2; C4: |.(SA.n - 2*(d*d)) + (SB.m - 2*(d*d)).| <= |.SA.n - 2*(d*d).| + |.SB.m - 2*(d*d).| by COMPLEX1:56; |.SA.n - 2*(d*d).| + |.SB.m - 2*(d*d).| < e/2 + e/2 by C1,C2,XREAL_1:8; hence thesis by C4,XXREAL_0:2; end; take k; thus thesis by B3; end; for p be Real st p > 0 ex k be Nat st for n, m be Nat st n >= k & m >= k holds ||.z.n - z.m.|| < p proof let p be Real; assume AS1: p > 0; then consider k be Nat such that D1: for n,m be Nat st n >= k & m >= k holds |. (SA.m + SB.n) - 4*(d*d) .| < p*p by A12; D2: for n, m be Nat st n >= k & m >= k holds ||.z.n - z.m.|| < p proof let n, m be Nat; assume n >= k & m >= k; then B0: |. (SA.m + SB.n) - 4*(d*d) .| < p*p by D1; set C=||.(x-z.n).||; set D=||.(x-z.m).||; B2: (x-z.n) + (x-z.m) = ((-z.n + x) + x) + -z.m by RLVECT_1:def 3 .= ((x + x) + -z.n) + -z.m by RLVECT_1:def 3 .= (x + x) +(-z.n + -z.m) by RLVECT_1:def 3 .= (x + x) + (-(z.n + z.m)) by RLVECT_1:31 .= (1*x + x) + (-(z.n + z.m)) by RLVECT_1:def 8 .= (1*x + 1*x) + (-(z.n + z.m)) by RLVECT_1:def 8 .= ((1+1)*x) + (-(z.n + z.m)) by RLVECT_1:def 6 .= 2*x - (z.n + z.m); B3: (x-z.n) - (x-z.m) = (x + -z.n) + (z.m + -x) by RLVECT_1:33 .= -x + ((x + -z.n) + z.m) by RLVECT_1:def 3 .= -x + (x + (-z.n + z.m)) by RLVECT_1:def 3 .= (-x + x) + (-z.n + z.m) by RLVECT_1:def 3 .= 0.X + (-z.n + z.m) by RLVECT_1:5 .= z.m - z.n; set E=||.2*x - (z.n + z.m).||; set F=||.z.m - z.n.||; B6: F*F = (E*E + F*F) + -E*E .= (2*(C*C) + 2*(D*D)) + -E*E by Lm88A,B2,B3; 2*x - (z.n + z.m) = 2*x + (-1)*(z.n + z.m) by RLVECT_1:16 .= 2*x + 2*(1/2)*(-(z.n + z.m)) by RLVECT_1:24 .= 2*x + 2*((1/2)*(-(z.n + z.m))) by RLVECT_1:def 7 .= 2*(x + (1/2)*(-(z.n + z.m))) by RLVECT_1:def 5 .= 2*(x - (1/2)*(z.n + z.m)) by RLVECT_1:25; then B7: ||.2*x - (z.n + z.m).|| = |.2.|*||.x - (1/2)*(z.n + z.m).|| by BHSP_1:27 .= 2*||.x - (1/2)*(z.n + z.m).|| by ABSVALUE:def 1; reconsider znm=z.n+z.m as Point of X; reconsider p0=||.x - (1/2)*(z.n+z.m).|| as Real; z.n in M & z.m in M by A8; then znm in M by RUSUB_1:14; then (1/2)*znm in M by RUSUB_1:15; then p0 in Y by A3; then d <= p0 by A3,A4,SEQ_4:def 2; then 2*d <= ||.2*x - (z.n + z.m).|| by B7,XREAL_1:64; then (2*d)*(2*d) <= ||.2*x - (z.n + z.m).||*||.2*x - (z.n + z.m).|| by A3,XREAL_1:66; then -(E*E) <= -(4*(d*d)) by XREAL_1:24; then B81: F*F <= (2*(C*C) + 2*(D*D)) + -(4*(d*d)) by B6,XREAL_1:6; E2: SA.n = 2*S1.n by SEQ_1:9 .= 2*((S.n)*(S.n)) by SEQ_1:8; E3: SB.m = 2*S2.m by SEQ_1:9 .= 2*((S.m)*(S.m)) by SEQ_1:8; B91: C = S.n & D = S.m by A8; (SA.n + SB.m) - 4*(d*d) <= |.(SA.n + SB.m) - 4*(d*d).| by ABSVALUE:4; then F*F <= |.(SA.n + SB.m) - 4*(d*d).| by B91,B81,E2,E3,XXREAL_0:2; then F*F < p*p by B0,XXREAL_0:2; then F^2 < p*p by SQUARE_1:def 1; then B10: F^2 < p^2 by SQUARE_1:def 1; 0 <= F*F by XREAL_1:63; then 0 <= F^2 by SQUARE_1:def 1; then B11: sqrt F^2 < sqrt p^2 by B10,SQUARE_1:27; B12: F < sqrt p^2 by B11,SQUARE_1:22,BHSP_1:28; ||.z.n - z.m.|| = ||.-(z.m - z.n).|| by RLVECT_1:33 .= F by BHSP_1:31; hence thesis by B12,SQUARE_1:22,AS1; end; take k; thus thesis by D2; end; then A13: z is convergent by BHSP_3:def 4,BHSP_3:2; then consider x0 be Point of X such that A14: for r be Real st r > 0 ex m be Nat st for n be Nat st n >= m holds ||.z.n - x0.|| < r by BHSP_2:9; lim z = x0 by A13,A14,BHSP_2:19; then A16: lim ||.z - x.|| = ||.x0-x.|| by A13,BHSP_2:34 .= ||.-(x0-x).|| by BHSP_1:31 .= ||.x-x0.|| by RLVECT_1:33; for y be object st y in rng z holds y in N proof let y be object; assume y in rng z; then ex n being object st n in NAT & z.n = y by FUNCT_2:11; then y in M by A8; hence thesis by A1; end; then rng z c= N; then BX: lim z in N by A1,A13,LM1; ex k0 be Nat st for n be Nat st k0 <= n holds S.n = ||.z - x.||.n proof set k0 = the Nat; B1: for n be Nat st k0 <= n holds S.n = ||.z - x.||.n proof let n be Nat; assume k0 <= n; thus S.n = ||.x - z.n.|| by A8 .= ||.-(z.n - x).|| by RLVECT_1:33 .= ||.z.n + -x.|| by BHSP_1:31 .= ||.(z + -x).n.|| by BHSP_1:def 6 .= ||.(z - x).n.|| by BHSP_1:56 .= ||.z - x.||.n by BHSP_2:def 3; end; take k0; thus thesis by B1; end; then BY: lim S = lim ||.z - x.|| by A5,SEQ_4:19; take x0; thus thesis by BX,A1,A13,A14,BHSP_2:19,BY,SEQ_2:def 7,B5,A16,A5; end; theorem Lm87A: for X be RealHilbertSpace, M be Subspace of X, x,x0 be Point of X, d be Real st x0 in M & (ex Y be non empty Subset of REAL st Y = {||.x-y.|| where y is Point of X: y in M} & d = lower_bound Y >= 0) holds d = ||.x-x0.|| iff for w be Point of X st w in M holds w, x-x0 are_orthogonal proof let X be RealHilbertSpace, M be Subspace of X, x,x0 be Point of X, d be Real; assume that A2: x0 in M and A3: ex Y be non empty Subset of REAL st Y = {||.x-y.|| where y is Point of X: y in M} & d = lower_bound Y >= 0; consider Y be non empty Subset of REAL such that A4: Y = {||.x-y.|| where y is Point of X: y in M} & d = lower_bound Y >= 0 by A3; reconsider r0=0 as Real; for r be ExtReal st r in Y holds r0 <= r proof let r be ExtReal; assume r in Y; then ex y be Point of X st r = ||.x-y.|| & y in M by A4; hence r0 <= r by BHSP_1:28; end; then r0 is LowerBound of Y by XXREAL_2:def 2; then A51: Y is bounded_below; A6: for y0 be Point of X st y0 in M holds d <= ||.x-y0.|| proof let y0 be Point of X; assume y0 in M; then ||.x-y0.|| in Y by A4; hence thesis by A51,A4,SEQ_4:def 2; end; hereby assume AS1: d = ||.x-x0.||; assume not (for w be Point of X st w in M holds w, x-x0 are_orthogonal); then consider w be Point of X such that B1: w in M & w .|. (x-x0) <> 0; set e = w .|. (x-x0); set r = e/||.w.||^2; set s = ||.w.||^2; reconsider w0 = x0 + r*w as Point of X; B21: r*w in M by B1,RUSUB_1:15; per cases; suppose C11: s = 0; ||.w.|| = 0 by C11,SQUARE_1:17,SQUARE_1:22,BHSP_1:28; then w = 0.X by BHSP_1:26; hence contradiction by B1,BHSP_1:14; end; suppose CS2: s <> 0; C2: ||.x-w0.||^2 = ||.(x-x0) - r*w.||^2 by RLVECT_1:27 .= ||.x-x0.||^2 - 2*((x-x0) .|. (r*w)) + ||.r*w.||^2 by RUSUB_5:29; C3: (x-x0) .|. (r*w) = (e/s)*e by BHSP_1:3 .= (e*e)/s by XCMPLX_1:74 .= e^2/s by SQUARE_1:def 1; C4: ||.r*w.||^2 = (|.r.|*||.w.||)^2 by BHSP_1:27 .= |.r.|^2*s by SQUARE_1:9 .= (e/s)^2*s by COMPLEX1:75 .= (e*(1/s))^2*s by XCMPLX_1:99 .= e^2*(1/s)^2*s by SQUARE_1:9 .= e^2*((1/s)^2*s) .= e^2*((1/s)*(1/s)*s) by SQUARE_1:def 1 .= e^2*((1/s)*((1/s)*s)) .= e^2*((1/s)*1) by CS2,XCMPLX_1:106 .= e^2/s by XCMPLX_1:99; C5: ||.x-w0.||^2 = ||.x-x0.||^2 - e^2/s by C3,C4,C2; C6: 0 < e^2 by B1,SQUARE_1:12; 0 <= ||.w.|| by BHSP_1:28; then 0 <= ||.w.||*||.w.||; then 0 < s by CS2,SQUARE_1:def 1; then C7: ||.x-w0.||^2 < ||.x-x0.||^2 by C5,XREAL_1:44,C6; 0 <= ||.x-w0.||*||.x-w0.|| by XREAL_1:63; then 0 <= ||.x-w0.||^2 by SQUARE_1:def 1; then sqrt ||.x-w0.||^2 < sqrt ||.x-x0.||^2 by C7,SQUARE_1:27; then C91: ||.x-w0.|| < sqrt ||.x-x0.||^2 by BHSP_1:28,SQUARE_1:22; d <= ||.x-w0.|| by A6,B21,A2,RUSUB_1:14; hence contradiction by C91,AS1,BHSP_1:28,SQUARE_1:22; end; end; assume AS2: for w be Point of X st w in M holds w, x-x0 are_orthogonal; B1: for y be Point of X st y in M holds ||.x-x0.|| <= ||.x-y.|| proof let y be Point of X; assume y in M; then C1: x0-y,x-x0 are_orthogonal by AS2,A2,RUSUB_1:17; x - y = (x - y) + 0.X .= (x + -y) + (-x0 + x0) by RLVECT_1:5 .= ((x + -y) + -x0) + x0 by RLVECT_1:def 3 .= ((x + -x0) + -y) + x0 by RLVECT_1:def 3 .= (x - x0) + (x0 - y) by RLVECT_1:def 3; then ||.x-y.||^2 = ||.x-x0.||^2 + ||.x0-y.||^2 by C1,RUSUB_5:30; then C2: ||.x-y.||^2 - ||.x0-y.||^2 = ||.x-x0.||^2; 0 <= ||.x0-y.||*||.x0-y.|| by XREAL_1:63; then C31: 0 <= ||.x0-y.||^2 by SQUARE_1:def 1; 0 <= ||.x-x0.||*||.x-x0.|| by XREAL_1:63; then 0 <= ||.x-x0.||^2 by SQUARE_1:def 1; then sqrt ||.x-x0.||^2 <= sqrt ||.x-y.||^2 by C31,C2,XREAL_1:43,SQUARE_1:26; then ||.x-x0.|| <= sqrt ||.x-y.||^2 by BHSP_1:28,SQUARE_1:22; hence ||.x-x0.|| <= ||.x-y.|| by BHSP_1:28,SQUARE_1:22; end; for s be Real st s in Y holds ||.x-x0.|| <= s proof let s be Real; assume s in Y; then consider y0 be Point of X such that C1: s = ||.x-y0.|| & y0 in M by A4; thus ||.x-x0.|| <= s by B1,C1; end; then B2: ||.x-x0.|| <= d by A4,SEQ_4:43; d <= ||.x-x0.|| by A2,A6; hence d = ||.x-x0.|| by B2,XXREAL_0:1; end; theorem Th87A: for X be RealHilbertSpace, M be Subspace of X, N be Subset of X, x be Point of X st N = the carrier of M & N is closed holds ex y,z be Point of X st y in M & z in Ort_Comp M & x = y + z proof let X be RealHilbertSpace, M be Subspace of X, N be Subset of X, x be Point of X; assume AS: N = the carrier of M & N is closed; set Y = {||.x-y.|| where y is Point of X: y in M}; Y c= REAL proof let z be object; assume z in Y; then consider y be Point of X such that B1: z = ||.x-y.|| & y in M; thus z in REAL by B1,XREAL_0:def 1; end; then reconsider Y as Subset of REAL; 0.X in M by RUSUB_1:11; then ||.x-0.X.|| in Y; then reconsider Y as non empty Subset of REAL; set d = lower_bound Y; A11: for r be Real st r in Y holds 0 <= r proof let r be Real; assume r in Y; then consider y be Point of X such that B2: r = ||.x-y.|| & y in M; thus 0 <= r by B2,BHSP_1:28; end; then A1: 0 <= d by SEQ_4:43; consider x0 be Point of X such that A2: d = ||.x-x0.|| & x0 in M by AS,Lm88,A11,SEQ_4:43; reconsider y=x0 as Point of X; reconsider z=x-x0 as Point of X; for w be Point of X st w in M holds w, x-x0 are_orthogonal by A1,A2,Lm87A; then B21: x-x0 in {v where v is VECTOR of X : for w be Point of X st w in M holds w, v are_orthogonal}; B3: y + z = (x0 + -x0) + x by RLVECT_1:def 3 .= x + 0.X by RLVECT_1:5 .= x; take y,z; thus thesis by A2,B21,RUSUB_5:def 3,B3; end; theorem for X be RealUnitarySpace, M be Subspace of X, x be Point of X, y1,y2,z1,z2 be Point of X st y1 in M & y2 in M & z1 in Ort_Comp M & z2 in Ort_Comp M & x = y1 + z1 & x = y2 + z2 holds y1 = y2 & z1 = z2 proof let X be RealUnitarySpace, M be Subspace of X, x be Point of X; let y1,y2,z1,z2 be Point of X; assume that A1: y1 in M & y2 in M & z1 in Ort_Comp M & z2 in Ort_Comp M and A2: x = y1 + z1 & x = y2 + z2; y1 + (z1 + -y2) = (y2 + z2) + -y2 by RLVECT_1:def 3,A2; then y1 + (-y2 + z1) = y2 + (-y2 + z2) by RLVECT_1:def 3; then (y1 + -y2) + z1 = y2 + (-y2 + z2) by RLVECT_1:def 3; then (y1 - y2) + z1 = (y2 + -y2) + z2 by RLVECT_1:def 3; then (y1 - y2) + z1 = z2 + 0.X by RLVECT_1:def 10; then (y1 - y2) + (z1 + -z1) = z2 + -z1 by RLVECT_1:def 3; then A31: (y1 - y2) + 0.X = z2 + -z1 by RLVECT_1:def 10; A4: y1 - y2 in M & z2 - z1 in Ort_Comp M by A1,RUSUB_1:17; then y1 - y2 in (the carrier of M) /\ the carrier of (Ort_Comp M) by XBOOLE_0:def 4,A31; then y1 - y2 = 0.X by Lm814; hence y1 = y2 by RLVECT_1:21; z2 - z1 in (the carrier of M) /\ the carrier of (Ort_Comp M) by A4,A31,XBOOLE_0:def 4; then z2 - z1 = 0.X by Lm814; hence z1 = z2 by RLVECT_1:21; end; begin :: F. Riesz Representation Theorem theorem for X be RealUnitarySpace, f be linear-Functional of X, y be Point of X st for x be Point of X holds f.x = x .|. y holds f is Lipschitzian proof let X be RealUnitarySpace, f be linear-Functional of X, y be Point of X; assume AS: for x be Point of X holds f.x = x .|. y; reconsider K=||.y.|| + 1 as Real; A11: 0 <= ||.y.|| by BHSP_1:28; for x be Point of X holds |.f.x.| <= K * ||.x.|| proof let x be Point of X; B1: |.x .|. y.| <= ||.x.||*||.y.|| by BHSP_1:29; B2: ||.y.|| < ||.y.|| + 1 by XREAL_1:145; 0 <= ||.x.|| by BHSP_1:28; then ||.y.|| * ||.x.|| <= (||.y.|| + 1) * ||.x.|| by B2,XREAL_1:64; then |.x .|. y.| <= (||.y.|| + 1) * ||.x.|| by B1,XXREAL_0:2; hence thesis by AS; end; hence thesis by A11,BHSP_6:def 4; end; KERX1: for X be RealUnitarySpace, f be Function of X,REAL st f is homogeneous holds f"{0} is non empty proof let X be RealUnitarySpace, f be Function of X,REAL; assume A1: f is homogeneous; f.(0.X) = f.(0 * 0.X) .= 0 * f.(0.X) by A1,HAHNBAN:def 3 .= 0; then f.(0.X) in {0} by TARSKI:def 1; hence thesis by FUNCT_2:38; end; registration let X be RealUnitarySpace, f be linear-Functional of X; cluster f"{0} -> non empty; correctness by KERX1; end; theorem KLXY1: for X be RealUnitarySpace, f be Function of X,REAL st f is additive homogeneous holds f"{0} is linearly-closed proof let X be RealUnitarySpace, f be Function of X,REAL; assume A1: f is additive homogeneous; set X1 = f"{0}; A2: for v,u be Point of X st v in X1 & u in X1 holds v+u in X1 proof let v,u be Point of X; assume AS1: v in X1 & u in X1; then v in the carrier of X & f.v in {0} by FUNCT_2:38; then A3: f.v = 0 by TARSKI:def 1; A4: u in the carrier of X & f.u in {0} by AS1,FUNCT_2:38; f.(v+u) = f.v + f.u by A1,HAHNBAN:def 2 .= 0 + 0 by A3,A4,TARSKI:def 1; then f.(v+u) in {0} by TARSKI:def 1; hence thesis by FUNCT_2:38; end; for r be Real, v be Point of X st v in X1 holds r*v in X1 proof let r be Real, v be Point of X; assume v in X1; then A5: v in the carrier of X & f.v in {0} by FUNCT_2:38; f.(r*v) = r * (f.v) by A1,HAHNBAN:def 3 .= r * 0 by A5,TARSKI:def 1; then f.(r*v) in {0} by TARSKI:def 1; hence thesis by FUNCT_2:38; end; hence thesis by A2; end; definition let X be RealUnitarySpace, f be linear-Functional of X; func UKer(f) -> strict Subspace of X means :defuker: the carrier of it = f"{0}; existence by KLXY1,RUSUB_1:29; uniqueness by RUSUB_1:24; end; theorem Lm89A: for X be RealUnitarySpace, f be linear-Functional of X st f is Lipschitzian holds f"{0} is closed proof let X be RealUnitarySpace, f be linear-Functional of X; assume AS: f is Lipschitzian; set Y=f"{0}; for s be sequence of X st rng s c= Y & s is convergent holds lim s in Y proof let s be sequence of X; assume B0: rng s c= Y & s is convergent; reconsider x0=lim s as Point of X; B1: dom f = the carrier of X by FUNCT_2:def 1; consider K be Real such that B3: 0 < K & for x be Point of X holds |. f.x .| <= K * ||. x .|| by AS,BHSP_6:def 4; for x1, x2 be Point of X st x1 in the carrier of X & x2 in the carrier of X holds |.f/.x1 - f/.x2.| <= K * ||.x1 - x2.|| proof let x1,x2 be Point of X; assume x1 in the carrier of X & x2 in the carrier of X; C1: |.f/.x1 - f/.x2.| = |.f.(x1 - x2).| by HAHNBAN:19; thus thesis by C1,B3; end; then f is_Lipschitzian_on (the carrier of X) by FUNCT_2:def 1,B3; then B41: f is_continuous_on (the carrier of X) by LM5; B5: rng s c= the carrier of X; B71: f is_continuous_in x0 by B41; B91: f/*s = f*s by B1,B5,FUNCT_2:def 11; ex k be Nat st for n be Nat st k <= n holds (f*s).n = (seq_const 0).n proof set k = the Nat; C0: for n be Nat st k <= n holds (f*s).n = (seq_const 0).n proof let n be Nat; assume k <= n; s.n in rng s by FUNCT_2:4,ORDINAL1:def 12; then D2: s.n in X & f.(s.n) in {0} by FUNCT_2:38,B0; dom s = NAT by FUNCT_2:def 1; then (f*s).n in {0} by ORDINAL1:def 12,D2,FUNCT_1:13; then (f*s).n = 0 by TARSKI:def 1; hence (f*s).n = (seq_const 0).n by SEQ_1:57; end; take k; thus thesis by C0; end; then lim (f*s) = lim (seq_const 0) by SEQ_4:19 .= (seq_const 0).0 by SEQ_4:26 .= 0; then f.x0 = 0 by B71,B0,B1,B91; then x0 in X & f.x0 in {0} by TARSKI:def 1; hence lim s in Y by FUNCT_2:38; end; hence f"{0} is closed by LM1; end; theorem Lm89B: for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of V st v <> 0.V holds v in Ort_Comp W implies not v in W proof let V be RealUnitarySpace; let W be Subspace of V; let v be VECTOR of V; assume A1: v <> 0.V; v in Ort_Comp W implies not v in W proof assume A2: v in Ort_Comp W; assume A3: v in W; v in {v1 where v1 is VECTOR of V : for w being VECTOR of V st w in W holds w,v1 are_orthogonal} by A2,RUSUB_5:def 3; then ex v1 being VECTOR of V st v = v1 & for w being VECTOR of V st w in W holds w,v1 are_orthogonal; then v,v are_orthogonal by A3; hence contradiction by A1,BHSP_1:def 2; end; hence thesis; end; theorem Th89A: for X be RealHilbertSpace, f be linear-Functional of X st f is Lipschitzian holds ex y be Point of X st for x be Point of X holds f.x = x .|. y proof let X be RealHilbertSpace, f be linear-Functional of X; assume AS: f is Lipschitzian; set M = UKer(f); A1: the carrier of M = f"{0} by defuker; per cases; suppose AS1: the carrier of X = the carrier of M; reconsider y=0.X as Point of X; B1: for x be Point of X holds f.x = x .|. y proof let x be Point of X; C11: x in X & f.x in {0} by FUNCT_2:38,AS1,A1; x .|. y = 0 by BHSP_1:15; hence thesis by C11,TARSKI:def 1; end; take y; thus thesis by B1; end; suppose the carrier of X <> the carrier of M; then not the carrier of X c= the carrier of M by RUSUB_1:def 1; then consider z be object such that B1: z in the carrier of X & not z in the carrier of M; reconsider y=z as Point of X by B1; reconsider N=the carrier of M as non empty Subset of X by A1; consider y1,z1 be Point of X such that C0: y1 in M & z1 in Ort_Comp M & 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 M 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=r*z1 as Point of X; C4: y in Ort_Comp M by C0,RUSUB_1:15; C5: for x be Point of X holds f.x = x .|. y proof let x be Point of X; set s=f.x/f.z1; reconsider y0=x - s*z1 as Point of X; D1: -s*z1 = (-1)*(s*z1) by RLVECT_1:16 .= ((-1)*s)*z1 by RLVECT_1:def 7; f.y0 = f.x + f.(((-1)*s)*z1) by D1,HAHNBAN:def 2 .= f.x + ((-1)*s)*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 M by defuker; y in {v where v is VECTOR of X : for w being VECTOR of X st w in M holds w, v are_orthogonal} by RUSUB_5:def 3,C4; then consider v be VECTOR of X such that D3: y = v & for w being VECTOR of X st w in M holds w, v are_orthogonal; D41: y0,y are_orthogonal by D2,D3; D6: (x - s*z1) .|. (r*z1) = x .|. (r*z1) - (s*z1) .|. (r*z1) by BHSP_1:11 .= r * x .|. z1 - (s*z1) .|. (r*z1) by BHSP_1:3 .= r * x .|. z1 - s * (z1 .|. (r*z1)) by BHSP_1:def 2; D7: s*r = f.x/||.z1.||^2 by C3,XCMPLX_1:98; D8: 0 <= z1 .|. z1 by BHSP_1:def 2; z1 .|. (r*z1) = r * (z1 .|. z1) by BHSP_1:3 .= r * ||.z1.||^2 by D8,SQUARE_1:def 2; then s * (z1 .|. (r*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; end; take y; thus thesis by C5; end; end; theorem for X be RealUnitarySpace, f be linear-Functional of X holds for y1,y2 be Point of X st for x be Point of X holds f.x = x .|. y1 & f.x = x .|. y2 holds y1 = y2 proof let X be RealUnitarySpace, f be linear-Functional of X; let y1,y2 be Point of X; assume AS: for x be Point of X holds f.x = x .|. y1 & f.x = x .|. y2; now let x be Point of X; f.x = x .|. y1 & f.x = x .|. y2 by AS; then x .|. y1 - x .|. y2 = 0; hence x .|. (y1 - y2) = 0 by BHSP_1:12; end; then (y1 - y2) .|. (y1 - y2) = 0; then y1 - y2 = 0.X by BHSP_1:def 2; hence y1 = y2 by RLVECT_1:21; end; theorem for X be RealHilbertSpace, f be Point of DualSp X, g be Lipschitzian linear-Functional of X st g=f holds ex y be Point of X st (for x be Point of X holds g.x = x .|. y) & ||.f.|| = ||.y.|| proof let X be RealHilbertSpace, f be Point of DualSp X, g be Lipschitzian linear-Functional of X; assume AS: g=f; consider y be Point of X such that A1: for x be Point of X holds g.x = x .|. y by Th89A; now let s be Real; assume s in PreNorms g; then consider t be VECTOR of X such that B1: s = |.g.t.| & ||.t.|| <= 1; B3: |.t .|. y.| <= ||.t.|| * ||.y.|| by BHSP_1:29; 0 <= ||.y.|| by BHSP_1:28; then ||.t.|| * ||.y.|| <= 1 * ||.y.|| by B1,XREAL_1:64; then |.t .|. y.| <= ||.y.|| by B3,XXREAL_0:2; hence s <= ||.y.|| by B1,A1; end; then upper_bound PreNorms g <= ||.y.|| by SEQ_4:45; then A2: ||.f.|| <= ||.y.|| by AS,Th24; A31: ||.y.|| <= ||.f.|| proof per cases; suppose ||.y.|| = 0; hence ||.y.|| <= ||.f.|| by Th27; end; suppose AS2: ||.y.|| <> 0; B1: 0 <= y .|. y by BHSP_1:def 2; B2: g.y = y .|. y by A1 .= ||.y.||^2 by B1,SQUARE_1:def 2 .= ||.y.|| * ||.y.|| by SQUARE_1:def 1; B3: g.y <= |.g.y.| by ABSVALUE:4; |.g.y.| <= ||.f.|| * ||.y.|| by AS,Th26; then B4: ||.y.|| * ||.y.|| <= ||.f.|| * ||.y.|| by B2,B3,XXREAL_0:2; B51: 0 <= ||.y.|| by BHSP_1:28; ||.y.|| * ||.y.||/||.y.|| = ||.y.|| & ||.f.|| * ||.y.||/||.y.|| = ||.f.|| by AS2,XCMPLX_1:89; hence ||.y.|| <= ||.f.|| by B51,B4,XREAL_1:72; end; end; take y; thus thesis by A1,A2,XXREAL_0:1,A31; end;