:: Bessel's Inequality
:: by Hiroshi Yamazaki , Yasunari Shidama and Yatsuka Nakamura
::
:: Received January 30, 2003
:: Copyright (c) 2003-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, BHSP_1, PRE_TOPC, SUBSET_1, FINSEQ_1, FUNCT_1, RELAT_1,
FUNCT_2, CARD_1, TARSKI, XBOOLE_0, BINOP_1, SETWISEO, FINSET_1, MEMBER_1,
FINSOP_1, ALGSTR_0, SUPINF_2, NAT_1, DECOMP_1, REAL_1, STRUCT_0, BINOP_2,
PROB_2, NORMSP_1, ARYTM_3, SQUARE_1, ARYTM_1, XXREAL_0, RVSUM_1,
RLVECT_1, ORDINAL4, BHSP_5;
notations TARSKI, SUBSET_1, XBOOLE_0, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0,
XXREAL_0, STRUCT_0, ALGSTR_0, REAL_1, XREAL_0, FUNCT_2, FINSET_1, NAT_1,
RELAT_1, BINOP_2, PRE_TOPC, RLVECT_1, BHSP_1, SQUARE_1, BINOP_1,
SETWISEO, FUNCT_1, FINSEQ_1, FINSOP_1;
constructors BINOP_1, DOMAIN_1, SETWISEO, REAL_1, SQUARE_1, NAT_1, BINOP_2,
MEMBERED, FINSOP_1, BHSP_1, RELSET_1, INT_1;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, FINSET_1,
NUMBERS, BINOP_2, STRUCT_0, CARD_1, XREAL_0, SQUARE_1, NAT_1, INT_1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions TARSKI;
equalities SQUARE_1, BINOP_1, RLVECT_1, ALGSTR_0;
expansions TARSKI;
theorems XBOOLE_0, SUBSET_1, BHSP_1, SQUARE_1, TARSKI, INT_1, FINSEQ_1,
FINSEQ_2, FINSEQ_3, FINSEQ_4, FUNCT_1, NAT_1, FUNCT_2, FINSOP_1,
HILBASIS, XBOOLE_1, BINOP_2, XREAL_1, XXREAL_0, RELAT_1, XREAL_0,
ORDINAL1;
schemes NAT_1, FINSEQ_1, FUNCT_2;
begin :: Sum of the result of operation with each element of a set
reserve X for RealUnitarySpace;
reserve x, y, y1, y2 for Point of X;
reserve xd for set;
reserve i, j, n for Nat;
theorem Th1:
for D being set, p1, p2 being FinSequence of D holds
p1 is one-to-one & p2 is one-to-one & rng p1 = rng p2 implies
dom p1 = dom p2 & ex P being Permutation of dom p1 st
p2 = p1*P & dom P = dom p1 & rng P = dom p1
proof
let D be set, p1, p2 be FinSequence of D;
assume that
A1: p1 is one-to-one and
A2: p2 is one-to-one and
A3: rng p1 = rng p2;
set P = p1"*p2;
len p1 = card rng p2 by A1,A3,FINSEQ_4:62
.= len p2 by A2,FINSEQ_4:62;
then
A4: dom p1 = Seg len p2 by FINSEQ_1:def 3
.= dom p2 by FINSEQ_1:def 3;
A5: now
let xd be object;
dom (p1") = rng p1 by A1,FUNCT_1:33;
then xd in dom p2 implies p2.xd in dom (p1") by A3,FUNCT_1:3;
hence xd in dom P iff xd in dom p2 by FUNCT_1:11;
end;
then
A6: dom P = dom p2 by TARSKI:2;
A7: rng(p1") = dom p1 by A1,FUNCT_1:33;
A8: rng P c= dom p1
by A7,FUNCT_1:14;
A9: dom p1 c= rng P
proof
let xd be object;
assume xd in dom p1;
then xd in rng(p1") by A1,FUNCT_1:33;
then consider yd being object such that
A10: yd in dom (p1") and
A11: xd = (p1").yd by FUNCT_1:def 3;
yd in rng p2 by A1,A3,A10,FUNCT_1:33;
then consider z being object such that
A12: z in dom p2 and
A13: yd = p2.z by FUNCT_1:def 3;
xd = P.z by A11,A12,A13,FUNCT_1:13;
hence thesis by A6,A12,FUNCT_1:def 3;
end;
A14: dom P = dom p1 by A4,A5,TARSKI:2;
A15: rng P = dom p1 by A8,A9,XBOOLE_0:def 10;
then P is Function of dom p1, dom p1 by A14,FUNCT_2:1;
then
A16: P is Permutation of dom p1 by A1,A2,A15,FUNCT_2:57;
now
let xd be object;
xd in dom P implies P.xd in dom p1 by A15,FUNCT_1:3;
hence xd in dom(p1*P) iff xd in dom p1 by A14,FUNCT_1:11;
end;
then
A17: dom p2 = dom (p1*P) by A4,TARSKI:2;
for xd being object st xd in dom p2 holds p2.xd = (p1*P).xd
proof
let xd be object;
assume
A18: xd in dom p2;
then
A19: p2.xd in rng p1 by A3,FUNCT_1:3;
(p1*P).xd = p1.((p1"*p2).xd) by A4,A14,A18,FUNCT_1:13
.= p1.((p1").(p2.xd)) by A18,FUNCT_1:13
.= p2.xd by A1,A19,FUNCT_1:35;
hence thesis;
end;
hence thesis by A4,A14,A15,A16,A17,FUNCT_1:2;
end;
definition
let DX be non empty set;
let f be BinOp of DX such that
A1: f is commutative associative and
A2: f is having_a_unity;
let Y be finite Subset of DX;
func f ++ Y -> Element of DX means
ex p being FinSequence of DX st p is one-to-one & rng p = Y & it = f "**" p;
existence
proof
consider p being FinSequence such that
A3: rng p = Y and
A4: p is one-to-one by FINSEQ_4:58;
reconsider q = p as FinSequence of DX by A3,FINSEQ_1:def 4;
ex p being FinSequence of DX st p is one-to-one &
rng p = Y & f "**" q = f "**" p by A3,A4;
hence thesis;
end;
uniqueness
proof
let X1,X2 be Element of DX such that
A5: ex p1 being FinSequence of DX st p1 is one-to-one &
rng p1 = Y & X1 = f "**" p1 and
A6: ex p2 being FinSequence of DX st p2 is one-to-one &
rng p2 = Y & X2 = f "**" p2;
consider p1 being FinSequence of DX such that
A7: p1 is one-to-one and
A8: rng p1 = Y and
A9: X1 = f "**" p1 by A5;
consider p2 being FinSequence of DX such that
A10: p2 is one-to-one and
A11: rng p2 = Y and
A12: X2 = f "**" p2 by A6;
ex P being Permutation of dom p1 st p2 = p1*P & dom P = dom p1 & rng P
= dom p1 by A7,A8,A10,A11,Th1;
hence thesis by A1,A2,A9,A12,FINSOP_1:7;
end;
end;
definition
let X;
let Y be finite Subset of X;
func setop_SUM(Y,X) -> set equals
(the addF of X) ++ Y if Y <> {} otherwise 0.X;
correctness;
end;
definition
let X, x;
let p be FinSequence;
let i be Nat;
func PO(i,p,x) -> set equals
(the scalar of X).[x,p.i];
correctness;
end;
definition
let DK, DX be non empty set;
let F be Function of DX, DK;
let p be FinSequence of DX;
func Func_Seq(F,p) -> FinSequence of DK equals
F*p;
correctness by FINSEQ_2:32;
end;
definition
let DK, DX be non empty set;
let f be BinOp of DK such that
A1: f is commutative associative and
A2: f is having_a_unity;
let Y be finite Subset of DX;
let F be Function of DX,DK;
A3: dom F = DX by FUNCT_2:def 1;
func setopfunc(Y,DX,DK,F,f) -> Element of DK means
:Def5:
ex p being FinSequence of DX st p is one-to-one &
rng p = Y & it = f "**" Func_Seq(F,p);
existence
proof
consider p being FinSequence such that
A4: rng p = Y and
A5: p is one-to-one by FINSEQ_4:58;
reconsider q = p as FinSequence of DX by A4,FINSEQ_1:def 4;
ex p being FinSequence of DX st p is one-to-one &
rng p = Y & f "**" Func_Seq(F,q) = f "**" Func_Seq(F,p) by A4,A5;
hence thesis;
end;
uniqueness
proof
let X1,X2 be Element of DK such that
A6: ex p1 being FinSequence of DX st p1 is one-to-one &
rng p1 = Y & X1 = f "**" Func_Seq(F,p1) and
A7: ex p2 being FinSequence of DX st p2 is one-to-one &
rng p2 = Y & X2 = f "**" Func_Seq(F,p2);
consider p1 being FinSequence of DX such that
A8: p1 is one-to-one and
A9: rng p1 = Y and
A10: X1 = f "**" Func_Seq(F,p1) by A6;
consider p2 being FinSequence of DX such that
A11: p2 is one-to-one and
A12: rng p2 = Y and
A13: X2 = f "**" Func_Seq(F,p2) by A7;
A14: dom p1 = dom p2 by A8,A9,A11,A12,Th1;
consider P being Permutation of dom p1 such that
A15: p2 = p1 * P and dom P = dom p1 and rng P = dom p1 by A8,A9,A11,A12,Th1;
now
let xd be object;
xd in dom p1 implies p1.xd in rng p1 by FUNCT_1:3;
hence xd in dom Func_Seq(F,p1) iff xd in dom p1 by A3,A9,FUNCT_1:11;
end;
then
A16: dom Func_Seq(F,p1) = dom p1 by TARSKI:2;
now
let xd be object;
xd in dom p2 implies p2.xd in rng p2 by FUNCT_1:3;
hence xd in dom(Func_Seq(F,p2)) iff xd in dom p2 by A3,A12,FUNCT_1:11;
end;
then
A17: dom Func_Seq(F,p2) = dom p2 by TARSKI:2;
A18: rng P = dom Func_Seq(F,p1) by A16,FUNCT_2:def 3;
now
let xd be object;
xd in dom P implies P.xd in dom Func_Seq(F,p1) by A18,FUNCT_1:3;
then xd in dom(Func_Seq(F,p1)*P) iff xd in dom P by FUNCT_1:11;
hence xd in dom(Func_Seq(F,p1)*P) iff xd in dom Func_Seq(F,p2)
by A14,A17,FUNCT_2:52;
end;
then
A19: dom Func_Seq(F,p2) = dom (Func_Seq(F,p1) * P) by TARSKI:2;
now
let s be object;
assume
A20: s in dom Func_Seq(F,p2);
then reconsider i=s as Element of NAT;
i in dom P by A14,A17,A20,FUNCT_2:52;
then
A21: P.i in rng P by FUNCT_1:3;
then P.i in dom(Func_Seq(F,p2)) by A14,A17,FUNCT_2:def 3;
then reconsider j=P.i as Element of NAT;
A22: j in dom p1 by A21,FUNCT_2:def 3;
A23: s in dom P by A14,A17,A20,FUNCT_2:52;
Func_Seq(F,p2).s = F.(p2.i) by A17,A20,FUNCT_1:13
.= F.(p1.(P.i)) by A15,A23,FUNCT_1:13
.= Func_Seq(F,p1).j by A22,FUNCT_1:13
.= (Func_Seq(F,p1) * P).s by A23,FUNCT_1:13;
hence Func_Seq(F,p2).s = (Func_Seq(F,p1) * P).s;
end;
then Func_Seq(F,p2) = Func_Seq(F,p1) * P by A19,FUNCT_1:2;
hence thesis by A1,A2,A10,A13,A16,FINSOP_1:7;
end;
end;
definition
let X, x;
let Y be finite Subset of X;
func setop_xPre_PROD(x,Y,X) -> Real means
ex p being FinSequence of the carrier of X st p is one-to-one & rng p = Y
& ex q being FinSequence of REAL st dom(q) = dom(p) &
(for i st i in dom q holds q.i = PO(i,p,x)) & it = addreal "**" q;
existence
proof
consider p0 being FinSequence such that
A1: rng p0 = Y and
A2: p0 is one-to-one by FINSEQ_4:58;
reconsider p = p0 as FinSequence of the carrier of X by A1,FINSEQ_1:def 4;
set ll = len p;
deffunc F(Nat) = PO($1,p,x);
consider q0 being FinSequence such that
A3: len q0 = ll & for i be Nat st i in dom q0 holds q0.i = F(i)
from FINSEQ_1:sch 2;
A4: dom q0 = Seg ll by A3,FINSEQ_1:def 3;
A5: dom q0 = dom p by A3,FINSEQ_3:29;
now
let i be Nat;
assume
A6: i in dom q0;
then
A7: q0.i = PO(i,p,x) by A3
.=(the scalar of X).[x,p.i];
reconsider y=p.i as Point of X by A5,A6,FINSEQ_2:11;
(the scalar of X).[x,p.i]= x .|. y by BHSP_1:def 1;
hence q0.i in REAL by A7,XREAL_0:def 1;
end;
then reconsider q = q0 as FinSequence of REAL by FINSEQ_2:12;
take addreal "**" q, p;
thus p is one-to-one & rng p = Y by A1,A2;
take q;
thus thesis by A3,A4,FINSEQ_1:def 3;
end;
uniqueness
proof
let X1, X2 be Real such that
A8: ex p1 being FinSequence of the carrier of X st p1 is one-to-one &
rng p1 = Y & ex q1 being FinSequence of REAL st dom q1 = dom p1 &
(for i st i in dom q1 holds q1.i = PO(i,p1,x)) & X1 = addreal "**" q1 and
A9: ex p2 being FinSequence of the carrier of X st p2 is one-to-one &
rng p2 = Y & ex q2 being FinSequence of REAL st dom q2 = dom p2 &
(for i st i in dom q2 holds q2.i = PO(i,p2,x)) & X2 = addreal "**" q2;
consider p1 being FinSequence of the carrier of X such that
A10: p1 is one-to-one and
A11: rng p1 = Y and
A12: ex q1 being FinSequence of REAL st dom(q1) = dom(p1) &
(for i st i in dom q1 holds q1.i = PO(i,p1,x)) &
X1 = addreal "**" q1 by A8;
consider p2 being FinSequence of the carrier of X such that
A13: p2 is one-to-one and
A14: rng p2 = Y and
A15: ex q2 being FinSequence of REAL st dom(q2) = dom(p2) &
(for i st i in dom q2 holds q2.i = PO(i,p2,x)) &
X2 = addreal "**" q2 by A9;
consider q1 being FinSequence of REAL such that
A16: dom q1 = dom p1 and
A17: for i st i in dom q1 holds q1.i = PO(i,p1,x) and
A18: X1 = addreal "**" q1 by A12;
consider q2 being FinSequence of REAL such that
A19: dom q2 = dom p2 and
A20: for i st i in dom q2 holds q2.i = PO(i,p2,x) and
A21: X2 = addreal "**" q2 by A15;
A22: dom p1 = dom p2 by A10,A11,A13,A14,Th1;
consider P being Permutation of dom p1 such that
A23: p2 = p1 * P and dom P = dom p1 and rng P = dom p1 by A10,A11,A13,A14,Th1;
A24: rng P = dom q1 by A16,FUNCT_2:def 3;
A25: dom P = dom q2 by A19,A22,FUNCT_2:52;
A26: rng P = dom q2 by A19,A22,FUNCT_2:def 3;
A27: dom p1 = dom q2 by A10,A11,A13,A14,A19,Th1;
now
let xd be object;
xd in dom P implies P.xd in dom q1 by A24,FUNCT_1:3;
hence xd in dom(q1*P) iff xd in dom q2 by A25,FUNCT_1:11;
end;
then
A28: dom q2 = dom (q1 * P) by TARSKI:2;
now
let s be object;
assume
A29: s in dom q2;
then reconsider i=s as Element of NAT;
P.i in dom q2 by A25,A26,A29,FUNCT_1:3;
then reconsider j=P.i as Element of NAT;
A30: s in dom P by A19,A22,A29,FUNCT_2:52;
q2.s = PO(i,p2,x) by A20,A29
.= PO(j,p1,x) by A23,A30,FUNCT_1:13
.= q1.(P.i) by A16,A17,A25,A26,A27,A29,FUNCT_1:3
.= (q1 * P).s by A30,FUNCT_1:13;
hence q2.s = (q1 * P).s;
end;
then q2 = q1 * P by A28,FUNCT_1:2;
hence thesis by A16,A18,A21,FINSOP_1:7;
end;
end;
definition
let X, x;
let Y be finite Subset of X;
func setop_xPROD(x,Y,X) -> Real equals
setop_xPre_PROD(x,Y,X) if Y <> {}
otherwise 0;
correctness;
end;
begin :: Orthogonal Family & Orthonormal Family
definition
let X;
mode OrthogonalFamily of X -> Subset of X means
:Def8:
for x, y st x in it & y in it & x <> y holds x.|.y = 0;
existence
proof
take {};
thus thesis by SUBSET_1:1;
end;
end;
theorem Th2:
{} is OrthogonalFamily of X
proof
A1: {} is Subset of X by SUBSET_1:1;
x in {} & y in {} & x <> y implies x.|.y = 0;
hence thesis by A1,Def8;
end;
registration
let X;
cluster finite for OrthogonalFamily of X;
existence
proof
take {};
thus thesis by Th2;
end;
end;
definition
let X;
mode OrthonormalFamily of X -> Subset of X means
:Def9:
it is OrthogonalFamily of X & for x st x in it holds x.|.x = 1;
existence
proof
take {};
thus thesis by Th2;
end;
end;
theorem Th3:
{} is OrthonormalFamily of X
proof
A1: {} is OrthogonalFamily of X by Th2;
x in {} implies x.|.x = 1;
hence thesis by A1,Def9;
end;
registration
let X;
cluster finite for OrthonormalFamily of X;
existence
proof
take {};
thus thesis by Th3;
end;
end;
theorem
x = 0.X iff for y holds x.|.y = 0
proof
now
assume for y holds x.|.y = 0;
then x.|.x = 0;
hence x = 0.X by BHSP_1:def 2;
end;
hence thesis by BHSP_1:14;
end;
begin :: Bessel's inequality
:: parallelogram law
theorem
||.x+y.||^2 + ||.x-y.||^2 = 2*||.x.||^2 + 2*||.y.||^2
proof
A1: (x+y).|.(x+y) >= 0 by BHSP_1:def 2;
A2: (x-y).|.(x-y) >= 0 by BHSP_1:def 2;
A3: x.|.x >= 0 by BHSP_1:def 2;
A4: y.|.y >= 0 by BHSP_1:def 2;
||.x+y.||^2 + ||.x-y.||^2
= (sqrt ((x+y).|.(x+y)))^2 + ||.x-y.||^2 by BHSP_1:def 4
.= ((x+y).|.(x+y)) + ||.x-y.||^2 by A1,SQUARE_1:def 2
.= ((x+y).|.(x+y)) + (sqrt ((x-y).|.(x-y)))^2 by BHSP_1:def 4
.= ((x+y).|.(x+y)) + ((x-y).|.(x-y)) by A2,SQUARE_1:def 2
.= x.|.x + 2*x.|.y + y.|.y + ((x-y).|.(x-y)) by BHSP_1:16
.= x.|.x + 2*x.|.y + y.|.y + (x.|.x - 2*x.|.y + y.|.y) by BHSP_1:18
.= 2 * x.|.x + 2 * y.|.y
.= 2*(sqrt(x.|.x))^2 + 2*(y.|.y) by A3,SQUARE_1:def 2
.= 2*(sqrt(x.|.x))^2 + 2*(sqrt(y.|.y))^2 by A4,SQUARE_1:def 2
.= 2*||.x.||^2 + 2*(sqrt(y.|.y))^2 by BHSP_1:def 4
.= 2*||.x.||^2 + 2*||.y.||^2 by BHSP_1:def 4;
hence thesis;
end;
:: The Pythagorean theorem
theorem
x, y are_orthogonal implies ||.x+y.||^2 = ||.x.||^2 + ||.y.||^2
proof
assume x, y are_orthogonal;
then
A1: x.|.y = 0 by BHSP_1:def 3;
A2: (x+y).|.(x+y) >= 0 by BHSP_1:def 2;
A3: x.|.x >= 0 by BHSP_1:def 2;
A4: y.|.y >= 0 by BHSP_1:def 2;
||.x+y.||^2 = (sqrt ((x+y).|.(x+y)))^2 by BHSP_1:def 4
.= (x+y).|.(x+y) by A2,SQUARE_1:def 2
.= x.|.x + 2*x.|.y + y.|.y by BHSP_1:16
.= (sqrt(x.|.x))^2 + y.|.y by A1,A3,SQUARE_1:def 2
.= (sqrt(x.|.x))^2 + (sqrt(y.|.y))^2 by A4,SQUARE_1:def 2
.= ||.x.||^2 + (sqrt(y.|.y))^2 by BHSP_1:def 4
.= ||.x.||^2 + ||.y.||^2 by BHSP_1:def 4;
hence thesis;
end;
theorem Th7:
for p be FinSequence of the carrier of X st (len p >=1 &
for i,j st i in dom p & j in dom p & i <> j
holds (the scalar of X).[p.i,p.j]=0) for q be FinSequence of REAL
st dom p = dom q &
(for i st i in dom q holds q.i = (the scalar of X).[(p.i),(p.i)])
holds ((the addF of X) "**" p).|. ((the addF of X) "**" p) = addreal "**" q
proof
let p be FinSequence of the carrier of X;
assume that
A1: len p >=1 and
A2: for i, j st i in dom p & j in dom p & i <> j holds (the scalar of
X).[(p.i),(p.j)]=0;
A3: 1 in dom p by A1,FINSEQ_3:25;
let q be FinSequence of REAL such that
A4: dom p = dom q and
A5: for i st i in dom q holds q.i = (the scalar of X).[(p.i),(p.i)];
consider f be sequence of the carrier of X such that
A6: f.1 = p.1 and
A7: for n be Nat st 0 <> n & n < len p
holds f.(n+1) = (the addF of X).(f.n, p.(n+1)) and
A8: (the addF of X) "**" p = f.(len p) by A1,FINSOP_1:1;
A9: ((the addF of X) "**" p).|. ((the addF of X) "**" p)
= (the scalar of X).[(f.(len p)), (f.(len p))] by A8,BHSP_1:def 1;
A10: Seg len q = dom p by A4,FINSEQ_1:def 3
.= Seg len p by FINSEQ_1:def 3;
then
A11: len q = len p by FINSEQ_1:6;
len q >= 1 by A1,A10,FINSEQ_1:6;
then consider g be sequence of REAL such that
A12: g.1 = q.1 and
A13: for n be Nat st 0 <> n & n < len q
holds g.(n + 1) = addreal.(g.n, q.(n + 1)) and
A14: addreal "**" q = g.(len q) by FINSOP_1:1;
defpred P[Nat] means
1 <= $1 & $1 <= len q implies g.$1 = (the scalar of X).[(f.$1), (f.$1)];
A15: P[0];
now
let n;
assume that
A16: 1 <= n & n <= len q implies g.n = (the scalar of X).[(f.n), (f.n)];
now
assume that
A17: 1 <= n+1 and
A18: n+1 <= len q;
A19: n <= n+1 by NAT_1:11;
per cases;
suppose
A20: n = 0;
1 in Seg len p by A1,FINSEQ_1:1;
then 1 in dom q by A4,FINSEQ_1:def 3;
hence g.(n+1) = (the scalar of X).[(f.(n+1)), (f.(n+1))]
by A5,A6,A12,A20;
end;
suppose
A21: n <> 0;
then 0 < n;
then
A22: 0 + 1 <= n by INT_1:7;
A23: n <= len p by A11,A18,A19,XXREAL_0:2;
A24: n + 1 - 1 < (len q) - 0 by A18,XREAL_1:15;
then
A25: n < len p by A10,FINSEQ_1:6;
A26: n + 1 in Seg len q by A17,A18,FINSEQ_1:1;
then
A27: n + 1 in dom q by FINSEQ_1:def 3;
A28: n + 1 in dom p by A4,A26,FINSEQ_1:def 3;
A29: n in NAT by ORDINAL1:def 12;
A30: dom f = NAT by FUNCT_2:def 1;
then
A31: f.n in rng f by FUNCT_1:3,A29;
rng f c= the carrier of X by RELAT_1:def 19;
then reconsider z = f.n as Element of X by A31;
A32: p.(n+1) in rng p by A28,FUNCT_1:3;
rng p c= the carrier of X by RELAT_1:def 19;
then reconsider y = p.(n+1) as Element of X by A32;
for i st 1 <= i & i <= n holds (the scalar of X).[f.i, y] = 0
proof
let i;
defpred P[Nat] means
1 <= $1 & $1 <= n implies (the scalar of X).[f.$1, y] = 0;
A33: P[0];
A34: for i st P[i] holds P[i+1]
proof
let i;
assume
A35: P[i];
A36: 1 <> n+1 by A21;
assume that
A37: 1 <= i+1 and
A38: i+1 <= n;
i + 1 <= len p by A23,A38,XXREAL_0:2;
then
A39: i+1 in dom p by A37,FINSEQ_3:25;
A40: i in NAT by ORDINAL1:def 12;
per cases;
suppose i = 0;
hence thesis by A2,A3,A6,A28,A36;
end;
suppose
A41: i <> 0;
A42: f.i in rng f by A30,FUNCT_1:3,A40;
rng f c= the carrier of X by RELAT_1:def 19;
then reconsider s = f.i as Element of X by A42;
A43: i+1 <= len p by A23,A38,XXREAL_0:2;
then i + 1 in dom p by A37,FINSEQ_3:25;
then
A44: p.(i+1) in rng p by FUNCT_1:3;
rng p c= the carrier of X by RELAT_1:def 19;
then reconsider t = p.(i+1) as Element of X by A44;
A45: i + 1 -1 < (len p) - 0 by A43,XREAL_1:15;
0 < i by A41;
then
A46: 0 + 1 <= i by INT_1:7;
i < i + 1 by XREAL_1:29;
then
A47: s.|.y = 0 by A35,A38,A46,BHSP_1:def 1,XXREAL_0:2;
A48: i+1 + 0 < n + 1 by A38,XREAL_1:8;
(the scalar of X).[f.(i+1), y]
= (the scalar of X).[s + t, y] by A7,A41,A45
.= (s + t).|.y by BHSP_1:def 1
.= 0 + (t.|.y) by A47,BHSP_1:2
.= (the scalar of X).[t, y] by BHSP_1:def 1
.= 0 by A2,A28,A39,A48;
hence thesis;
end;
end;
for i holds P[i] from NAT_1:sch 2(A33, A34);
hence thesis;
end;
then
A49: 0 = (the scalar of X).[z, y] by A22
.= z.|.y by BHSP_1:def 1;
thus g.(n+1) = addreal.((the scalar of X).[f.n,f.n], q.(n+1))
by A13,A16,A22,A24
.= addreal.((the scalar of X).[f.n, f.n],
(the scalar of X).[(p.(n+1)), (p.(n+1))]) by A5,A27
.= addreal.((the scalar of X).[f.n,f.n], y.|.y) by BHSP_1:def 1
.= addreal.(z.|.z, y.|.y) by BHSP_1:def 1
.= (z.|.z) + (z.|.y) + (y.|.z) + (y.|.y) by A49,BINOP_2:def 9
.= (z.|.(z+y)) + (y.|.z) + (y.|.y) by BHSP_1:2
.= (z.|.(z+y)) + ((y.|.z) + (y.|.y))
.= (z.|.(z+y)) + (y.|.(z+y)) by BHSP_1:2
.= (z+y).|.(z+y) by BHSP_1:2
.= (the scalar of X).[(the addF of X).(f.n, p.(n + 1)), z+y] by
BHSP_1:def 1
.= (the scalar of X).[(the addF of X).(f.n, p.(n + 1)),
f.(n+1)] by A7,A21,A25
.= (the scalar of X).[f.(n+1), f.(n+1)] by A7,A21,A25;
end;
end;
hence 1 <= n+1 & n+1 <= len q implies
g.(n+1) = (the scalar of X).[f.(n+1),f.(n+1)];
end;
then
A50: P[n] implies P[n+1];
for n holds P[n] from NAT_1:sch 2(A15,A50);
hence thesis by A1,A9,A11,A14;
end;
theorem Th8:
for p be FinSequence of the carrier of X st len p >= 1
for q be FinSequence of REAL st dom p = dom q &
(for i st i in dom q holds q.i = (the scalar of X).[x,p.i])
holds x.|.((the addF of X) "**" p) = addreal "**" q
proof
let p be FinSequence of the carrier of X such that
A1: len p >= 1;
let q be FinSequence of REAL such that
A2: dom p = dom q and
A3: for i st i in dom q holds q.i = (the scalar of X).[x,p.i];
consider f be sequence of the carrier of X such that
A4: f.1 = p.1 and
A5: for n be Nat st 0 <> n & n < len p holds
f.(n + 1) = (the addF of X).(f.n,p.(n + 1)) and
A6: (the addF of X) "**" p = f.len p by A1,FINSOP_1:1;
A7: Seg len q = dom p by A2,FINSEQ_1:def 3
.= Seg len p by FINSEQ_1:def 3;
then
A8: len q = len p by FINSEQ_1:6;
len q >= 1 by A1,A7,FINSEQ_1:6;
then consider g be sequence of REAL such that
A9: g.1 = q.1 and
A10: for n be Nat st 0 <> n & n < len q holds
g.(n + 1) = addreal.(g.n,q.(n + 1)) and
A11: addreal "**" q = g.len q by FINSOP_1:1;
defpred P[Nat] means
1 <= $1 & $1 <= len q implies g.$1 = (the scalar of X).[x,f.$1];
A12: P[0];
now
let n;
assume
A13: P[n];
now
assume that
A14: 1 <= n+1 and
A15: n+1 <= len q;
per cases;
suppose
A16: n=0;
1 in Seg len p by A1,FINSEQ_1:1;
then 1 in dom q by A2,FINSEQ_1:def 3;
hence g.(n+1) = (the scalar of X).[x,f.(n+1)] by A3,A4,A9,A16;
end;
suppose
A17: n<>0;
then 0 < n;
then
A18: 0+1 <= n by INT_1:7;
A19: n+1-1 < len q-0 by A15,XREAL_1:15;
A20: n+1 in Seg len q by A14,A15,FINSEQ_1:1;
then
A21: n+1 in dom q by FINSEQ_1:def 3;
A22: n+1 in dom p by A2,A20,FINSEQ_1:def 3;
A23: n in NAT by ORDINAL1:def 12;
dom f = NAT by FUNCT_2:def 1;
then
A24: f.n in rng f by FUNCT_1:3,A23;
rng f c= the carrier of X by RELAT_1:def 19;
then reconsider z=f.n as Element of X by A24;
A25: p.(n+1) in rng p by A22,FUNCT_1:3;
rng p c= the carrier of X by RELAT_1:def 19;
then reconsider y=p.(n+1) as Element of X by A25;
thus g.(n+1) = addreal.((the scalar of X).[x,f.n],q.(n + 1))
by A10,A13,A18,A19
.=addreal.((the scalar of X).[x,f.n],
(the scalar of X).[x,p.(n+1)]) by A3,A21
.=addreal.((the scalar of X).[x,f.n], (x .|. y)) by BHSP_1:def 1
.=addreal.( (x.|.z ),(x .|. y)) by BHSP_1:def 1
.= (x.|.z ) + (x.|.y) by BINOP_2:def 9
.= x .|. (z+y) by BHSP_1:2
.= (the scalar of X). [x,(the addF of X).(f.n,p.(n + 1))] by
BHSP_1:def 1
.= (the scalar of X). [x,f.(n + 1)] by A5,A8,A17,A19;
end;
end;
hence 1 <= n+1 & n+1 <= len q implies
g.(n+1) = (the scalar of X).[x,f.(n+1)];
end;
then
A26: P[n] implies P[n+1];
A27: for n holds P[n] from NAT_1:sch 2(A12,A26);
1 <=len q by A1,A7,FINSEQ_1:6;
then g.len q = (the scalar of X).[x,f.len q] by A27
.= (the scalar of X).[x,f.len p] by A7,FINSEQ_1:6;
hence thesis by A6,A11,BHSP_1:def 1;
end;
theorem Th9:
for S be finite non empty Subset of X
for F be Function of the carrier of X, the carrier of X
st S c= dom F & (for y1,y2 st y1 in S & y2 in S & y1 <> y2
holds (the scalar of X).[F.y1,F.y2] = 0)
for H be Function of the carrier of X, REAL
st S c= dom H & (for y st y in S holds H.y= (the scalar of X).[F.y,F.y])
for p be FinSequence of the carrier of X
st p is one-to-one & rng p = S holds
(the scalar of X).[(the addF of X) "**" Func_Seq(F,p),
(the addF of X) "**" Func_Seq(F,p)] = addreal "**" Func_Seq(H,p)
proof
let S be finite non empty Subset of X;
let F be Function of the carrier of X, the carrier of X such that
A1: S c= dom F and
A2: for y1, y2 st y1 in S & y2 in S & y1 <> y2 holds (the scalar of X).
[F.y1, F.y2]=0;
let H be Function of the carrier of X, REAL such that
A3: S c= dom H and
A4: for y st y in S holds H.y = (the scalar of X).[F.y, F.y];
let p be FinSequence of the carrier of X such that
A5: p is one-to-one and
A6: rng p = S;
set fp = Func_Seq(F, p);
set hp = Func_Seq(H, p);
now
let z be object;
z in dom p implies p.z in rng p by FUNCT_1:3;
hence z in dom fp iff z in dom p by A1,A6,FUNCT_1:11;
end;
then
A7: dom fp = dom p by TARSKI:2;
then
A8: Seg len p = dom fp by FINSEQ_1:def 3
.= Seg len fp by FINSEQ_1:def 3;
A9: len p = card S by A5,A6,FINSEQ_4:62;
0 < card S;
then 0+1 <= card S by INT_1:7;
then
A10: 1 <= len fp by A8,A9,FINSEQ_1:6;
A11: for i, j st i in dom fp & j in dom fp & i <> j
holds (the scalar of X).[fp.i, fp.j] = 0
proof
let i, j;
assume that
A12: i in dom fp and
A13: j in dom fp and
A14: i <> j;
A15: p.i in S by A6,A7,A12,FUNCT_1:3;
A16: p.j in S by A6,A7,A13,FUNCT_1:3;
A17: fp.i = F.(p.i) by A12,FUNCT_1:12;
A18: fp.j = F.(p.j) by A13,FUNCT_1:12;
p.i <> p.j by A5,A7,A12,A13,A14,FUNCT_1:def 4;
hence thesis by A2,A15,A16,A17,A18;
end;
now
let z be object;
z in dom p implies p.z in rng p by FUNCT_1:3;
hence z in dom hp iff z in dom p by A3,A6,FUNCT_1:11;
end;
then
A19: dom hp = dom p by TARSKI:2;
A20: for i st i in dom hp holds hp.i = (the scalar of X).[fp.i, fp.i]
proof
let i such that
A21: i in dom hp;
A22: p.i in S by A6,A19,A21,FUNCT_1:3;
hp.i = H.(p.i) by A19,A21,FUNCT_1:13
.= (the scalar of X).[F.(p.i), F.(p.i)] by A4,A22
.= (the scalar of X).[(F*p).i, F.(p.i)] by A19,A21,FUNCT_1:13
.= (the scalar of X).[fp.i, fp.i] by A19,A21,FUNCT_1:13;
hence thesis;
end;
(the scalar of X).[(the addF of X) "**" Func_Seq(F, p),
(the addF of X) "**" Func_Seq(F, p)]
= ((the addF of X) "**" fp).|.((the addF of X) "**" fp) by BHSP_1:def 1
.= addreal "**" Func_Seq(H,p) by A7,A10,A11,A19,A20,Th7;
hence thesis;
end;
theorem Th10:
for S be finite non empty Subset of X
for F be Function of the carrier of X, the carrier of X st S c= dom F
for H be Function of the carrier of X, REAL
st S c= dom H & (for y st y in S holds H.y = (the scalar of X).[x,F.y])
for p be FinSequence of the carrier of X st p is one-to-one & rng p = S
holds (the scalar of X).[x,(the addF of X) "**" Func_Seq(F,p) ]
= addreal "**" Func_Seq(H,p)
proof
let S be finite non empty Subset of X;
let F be Function of the carrier of X, the carrier of X such that
A1: S c= dom F;
let H be Function of the carrier of X, REAL such that
A2: S c= dom H and
A3: for y st y in S holds H.y = (the scalar of X).[x,(F.y)];
let p be FinSequence of the carrier of X such that
A4: p is one-to-one and
A5: rng p = S;
set p1=Func_Seq(F,p);
set q1=Func_Seq(H,p);
now
let xd be object;
xd in dom p implies p.xd in rng p by FUNCT_1:3;
hence xd in dom Func_Seq(F,p) iff xd in dom p by A1,A5,FUNCT_1:11;
end;
then
A6: dom Func_Seq(F,p)=dom p by TARSKI:2;
now
let xd be object;
xd in dom p implies p.xd in rng p by FUNCT_1:3;
hence xd in dom(Func_Seq(H,p)) iff xd in dom p by A2,A5,FUNCT_1:11;
end;
then
A7: dom Func_Seq(H,p)=dom p by TARSKI:2;
A8: for i st i in dom p1 holds q1.i = (the scalar of X).[x,(p1.i)]
proof
let i such that
A9: i in dom p1;
A10: p.i in S by A5,A6,A9,FUNCT_1:3;
q1.i = H.(p.i) by A6,A9,FUNCT_1:13
.= (the scalar of X).[x,(F.(p.i))] by A3,A10
.= (the scalar of X).[x,(p1.i)] by A6,A9,FUNCT_1:13;
hence thesis;
end;
A11: Seg len p = dom(Func_Seq(F,p)) by A6,FINSEQ_1:def 3
.= Seg len Func_Seq(F,p) by FINSEQ_1:def 3;
A12: len p = card S by A4,A5,FINSEQ_4:62;
0 < card S;
then 0+1 <= card S by INT_1:7;
then len Func_Seq(F,p) >= 1 by A11,A12,FINSEQ_1:6;
then x.|.((the addF of X) "**" p1) = addreal "**" q1 by A6,A7,A8,Th8;
hence thesis by BHSP_1:def 1;
end;
theorem Th11:
for X st the addF of X is commutative associative &
the addF of X is having_a_unity for x
for S be finite OrthonormalFamily of X st S is non empty
for H be Function of the carrier of X, REAL st
S c= dom H & (for y st y in S holds H.y= (x.|.y)^2)
for F be Function of the carrier of X, the carrier of X st
S c= dom F & (for y st y in S holds F.y = (x.|.y)*y) holds
x.|.setopfunc(S, the carrier of X, the carrier of X, F, the addF of X)
= setopfunc(S, the carrier of X, REAL, H, addreal)
proof
let X such that
A1: the addF of X is commutative associative and
A2: the addF of X is having_a_unity;
let x;
let S be finite OrthonormalFamily of X such that
A3: S is non empty;
let H be Function of the carrier of X, REAL such that
A4: S c= dom H and
A5: for y st y in S holds H.y= (x.|.y)^2;
let F be Function of the carrier of X, the carrier of X such that
A6: S c= dom F and
A7: for y st y in S holds F.y = (x.|.y)*y;
consider p be FinSequence of the carrier of X such that
A8: p is one-to-one and
A9: rng p = S and
A10: setopfunc(S, the carrier of X, the carrier of X, F, the addF of X)
= (the addF of X) "**" Func_Seq(F,p) by A1,A2,Def5;
A11: for y st y in S holds H.y = (the scalar of X).[x,(F.y)]
proof
let y such that
A12: y in S;
set a = x.|.y;
H.y = (x.|.y)^2 by A5,A12
.= x.|.(a*y) by BHSP_1:3
.= (the scalar of X).[x,(a*y)] by BHSP_1:def 1
.= (the scalar of X).[x,(F.y)] by A7,A12;
hence thesis;
end;
A13: setopfunc(S, the carrier of X, REAL, H, addreal)
= addreal "**" Func_Seq(H,p) by A8,A9,Def5;
x.|.setopfunc(S, the carrier of X, the carrier of X, F, the addF of X)
= (the scalar of X).[x,(the addF of X) "**" Func_Seq(F,p)]
by A10,BHSP_1:def 1;
hence thesis by A3,A4,A6,A8,A9,A11,A13,Th10;
end;
theorem Th12:
for X st the addF of X is commutative associative &
the addF of X is having_a_unity
for x for S be finite OrthonormalFamily of X st S is non empty
for F be Function of the carrier of X, the carrier of X
st S c= dom F & (for y st y in S holds F.y = (x.|.y)*y)
for H be Function of the carrier of X, REAL
st S c= dom H & (for y st y in S holds H.y= (x.|.y)^2) holds
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, REAL, H, addreal)
proof
let X such that
A1: the addF of X is commutative associative and
A2: the addF of X is having_a_unity;
let x;
let S be finite OrthonormalFamily of X such that
A3: S is non empty;
let F be Function of the carrier of X, the carrier of X such that
A4: S c= dom F and
A5: for y st y in S holds F.y = (x.|.y)*y;
let H be Function of the carrier of X, REAL such that
A6: S c= dom H and
A7: for y st y in S holds H.y= (x.|.y)^2;
consider p be FinSequence of the carrier of X such that
A8: p is one-to-one and
A9: rng p = S and
A10: setopfunc(S, the carrier of X, the carrier of X, F, the addF of X) =
(the addF of X) "**" Func_Seq(F, p) by A1,A2,Def5;
A11: for y1, y2 st y1 in S & y2 in S & y1 <> y2
holds (the scalar of X).[F.y1, F.y2] = 0
proof
let y1, y2;
assume that
A12: y1 in S and
A13: y2 in S and
A14: y1 <> y2;
set z1 = x.|.y1;
set z2 = x.|.y2;
S is OrthogonalFamily of X by Def9;
then
A15: y1.|.y2 = 0 by A12,A13,A14,Def8;
(the scalar of X).[F.y1, F.y2]
= (the scalar of X).[(x.|.y1)*y1, F.y2] by A5,A12
.= (the scalar of X).[(x.|.y1)*y1, (x.|.y2)*y2] by A5,A13
.= (z1*y1) .|. (z2*y2) by BHSP_1:def 1
.= z2 * (y2 .|. (z1*y1)) by BHSP_1:3
.= z2 * (z1 * (y2 .|. y1)) by BHSP_1:3
.= 0 by A15;
hence thesis;
end;
A16: for y st y in S holds H.y = (the scalar of X).[F.y, F.y]
proof
let y;
assume
A17: y in S;
then
A18: F.y = ((x.|.y) * y) by A5;
H.y = (x.|.y)^2 by A7,A17
.= (x.|.y) * (x.|.y) * 1
.= (x.|.y) * (x.|.y) * (y.|.y) by A17,Def9
.= (x.|.y) * ((x.|.y) * (y.|.y))
.= (x.|.y) * (((x.|.y) * y).|.y) by BHSP_1:3
.= (((x.|.y) * y).|.((x.|.y) * y)) by BHSP_1:3
.= (the scalar of X).[F.y, F.y] by A18,BHSP_1:def 1;
hence thesis;
end;
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)
= (the scalar of X).[(the addF of X) "**" Func_Seq(F, p),
(the addF of X) "**" Func_Seq(F, p)] by A10,BHSP_1:def 1
.= addreal "**" Func_Seq(H, p) by A3,A4,A6,A8,A9,A11,A16,Th9
.= setopfunc(S, the carrier of X, REAL, H, addreal) by A8,A9,Def5;
hence thesis;
end;
theorem
for X st the addF of X is commutative associative &
the addF of X is having_a_unity for x
for S be finite OrthonormalFamily of X st S is non empty
for H be Function of the carrier of X, REAL
st S c= dom H & (for y st y in S holds H.y = (x.|.y)^2) holds
setopfunc(S, the carrier of X, REAL, H, addreal) <= ||.x.||^2
proof
let X such that
A1: the addF of X is commutative associative and
A2: the addF of X is having_a_unity;
let x;
let S be finite OrthonormalFamily of X such that
A3: S is non empty;
let H be Function of the carrier of X, REAL such that
A4: S c= dom H and
A5: for y st y in S holds H.y= (x.|.y)^2;
now
deffunc F(object) = (the Mult of X) .[(the scalar of X).[x,$1],$1];
A6: for y be object st y in the carrier of X holds F(y) in the carrier of X
proof
let y be object such that
A7: y in the carrier of X;
reconsider y1 = y as Point of X by A7;
set x1 = x;
(the scalar of X).[x,y] = x1.|.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 thesis;
end;
ex F0 being Function of the carrier of X,the carrier of X
st for y be object st y in the carrier of X holds F0.y=F(y) from
FUNCT_2:sch 2(A6);
then consider F0 be Function of the carrier of X, the carrier of X such
that
A8: for y be 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
let y such that y in S;
thus F0.y = (the Mult of X).[(the scalar of X).[x,y],y] by A8
.= (x.|.y)*y by BHSP_1:def 1;
end;
then consider F be Function of the carrier of X, the carrier of X
such that
A10: S c= dom F and
A11: for y 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);
z.|.x = setopfunc(S, the carrier of X, REAL, H, addreal)
by A1,A2,A3,A4,A5,A10,A11,Th11;
then x.|.z = z.|.z by A1,A2,A3,A4,A5,A10,A11,Th12;
then (x - z).|.(x - z) = ((x.|.x - z.|.z) - z.|.z ) + z.|.z 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;
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 thesis by BHSP_1:def 4;
end;
theorem
for DK, DX be non empty set
for f be BinOp of DK st f is commutative associative & f is having_a_unity
for Y1, Y2 be finite Subset of DX st Y1 misses Y2
for F be Function of DX, DK st Y1 c= dom F & Y2 c= dom F
for Z be finite Subset of DX st Z = Y1 \/ Y2 holds setopfunc(Z,DX,DK,F,f)
= f.(setopfunc(Y1,DX,DK,F,f), setopfunc(Y2,DX,DK,F,f))
proof
let DK, DX be non empty set;
let f be BinOp of DK such that
A1: f is commutative associative and
A2: f is having_a_unity;
let Y1, Y2 be finite Subset of DX such that
A3: Y1 misses Y2;
let F be Function of DX,DK such that
A4: Y1 c= dom F and
A5: Y2 c= dom F;
let Z be finite Subset of DX;
assume
A6: Z = Y1 \/ Y2;
consider p1 be FinSequence of DX such that
A8: p1 is one-to-one and
A9: rng p1 = Y1 and
A10: setopfunc(Y1, DX,DK, F, f) = f "**" Func_Seq(F,p1) by A1,A2,Def5;
consider p2 be FinSequence of DX such that
A11: p2 is one-to-one and
A12: rng p2 = Y2 and
A13: setopfunc(Y2, DX,DK, F, f) = f "**" Func_Seq(F,p2) by A1,A2,Def5;
set q = p1^p2;
A14: q is one-to-one by A3,A8,A9,A11,A12,FINSEQ_3:91;
rng q = Z by A6,A9,A12,FINSEQ_1:31;
then
A15: setopfunc(Z, DX, DK, F, f) = f "**" Func_Seq(F,q) by A1,A2,A14,Def5;
ex fp1, fp2 be FinSequence st fp1 = F*p1 & fp2 = F*p2 & F*(p1^p2) = fp1^fp2
by A4,A5,A6,A9,A12,HILBASIS:1,XBOOLE_1:8;
hence thesis by A1,A2,A10,A13,A15,FINSOP_1:5;
end;