let m be non trivial Nat; for p being Jpolynom of m, F_Complex
for f being FinSequence of REAL
for xf, cxf being Function of m,F_Complex st xf = FS2XFS f & cxf = FS2XFS (_sqrt f) holds
eval (p,cxf) = eval ((JsqrtSeries p),xf)
let p be Jpolynom of m, F_Complex ; for f being FinSequence of REAL
for xf, cxf being Function of m,F_Complex st xf = FS2XFS f & cxf = FS2XFS (_sqrt f) holds
eval (p,cxf) = eval ((JsqrtSeries p),xf)
reconsider L = F_Complex as Field ;
let f be FinSequence of REAL ; for xf, cxf being Function of m,F_Complex st xf = FS2XFS f & cxf = FS2XFS (_sqrt f) holds
eval (p,cxf) = eval ((JsqrtSeries p),xf)
let xf, cxf be Function of m,F_Complex; ( xf = FS2XFS f & cxf = FS2XFS (_sqrt f) implies eval (p,cxf) = eval ((JsqrtSeries p),xf) )
assume A1:
( xf = FS2XFS f & cxf = FS2XFS (_sqrt f) )
; eval (p,cxf) = eval ((JsqrtSeries p),xf)
reconsider xfL = xf, cxfL = cxf as Function of m,L ;
m > 1
by NEWTON03:def 1;
then A2:
for b being bag of m
for n being Nat st b in Support p holds
b . n is even
by Def10;
set c = JsqrtSeries p;
reconsider P = p, C = JsqrtSeries p as Polynomial of m,L ;
set CS = SgmX ((BagOrder m),(Support C));
consider Cy being FinSequence of L such that
A3:
( len Cy = len (SgmX ((BagOrder m),(Support C))) & eval (C,xfL) = Sum Cy )
and
A4:
for i being Element of NAT st 1 <= i & i <= len Cy holds
Cy /. i = ((C * (SgmX ((BagOrder m),(Support C)))) /. i) * (eval (((SgmX ((BagOrder m),(Support C))) /. i),xfL))
by POLYNOM2:def 4;
BagOrder m linearly_orders Support C
by POLYNOM2:18;
then A5:
( rng (SgmX ((BagOrder m),(Support C))) = Support C & SgmX ((BagOrder m),(Support C)) is one-to-one )
by PRE_POLY:def 2, PRE_POLY:10;
then consider S being one-to-one FinSequence of Bags m such that
A6:
( len S = len (SgmX ((BagOrder m),(Support C))) & rng S = Support p )
and
A7:
for i being Nat st i in dom S holds
S . i = (2 (#) ((SgmX ((BagOrder m),(Support C))) /. i)) +* (0,(((SgmX ((BagOrder m),(Support C))) /. i) . 0))
by A2, Th65;
consider y being FinSequence of L such that
A8:
( len y = card (Support p) & eval (P,cxfL) = Sum y )
and
A9:
for i being Nat st 1 <= i & i <= len y holds
y /. i = ((P * S) /. i) * (eval ((S /. i),cxfL))
by A6, HILB10_2:24;
A10:
card (Support p) = len S
by A6, FINSEQ_4:62;
for i being Nat st 1 <= i & i <= len y holds
y . i = Cy . i
proof
let i be
Nat;
( 1 <= i & i <= len y implies y . i = Cy . i )
assume A11:
( 1
<= i &
i <= len y )
;
y . i = Cy . i
A12:
i in NAT
by ORDINAL1:def 12;
(
rng (SgmX ((BagOrder m),(Support C))) c= Bags m &
Bags m = dom C )
by A5, FUNCT_2:def 1;
then A13:
dom (C * (SgmX ((BagOrder m),(Support C)))) = dom (SgmX ((BagOrder m),(Support C)))
by RELAT_1:27;
(
rng S c= Bags m &
Bags m = dom P )
by A6, FUNCT_2:def 1;
then A14:
dom (P * S) = dom S
by RELAT_1:27;
A15:
(
i in dom (SgmX ((BagOrder m),(Support C))) &
i in dom S &
i in dom y &
i in dom Cy )
by A11, A10, A3, A6, A8, FINSEQ_3:25;
A16:
(
(P * S) /. i = (P * S) . i &
(P * S) . i = P . (S . i) &
S . i = S /. i )
by A14, A11, A10, A8, FINSEQ_3:25, PARTFUN1:def 6, FUNCT_1:12;
A17:
(
(C * (SgmX ((BagOrder m),(Support C)))) /. i = (C * (SgmX ((BagOrder m),(Support C)))) . i &
(C * (SgmX ((BagOrder m),(Support C)))) . i = C . ((SgmX ((BagOrder m),(Support C))) . i) &
(SgmX ((BagOrder m),(Support C))) . i = (SgmX ((BagOrder m),(Support C))) /. i )
by A13, A11, A10, A6, A8, FINSEQ_3:25, PARTFUN1:def 6, FUNCT_1:12;
A18:
S . i = (2 (#) ((SgmX ((BagOrder m),(Support C))) /. i)) +* (
0,
(((SgmX ((BagOrder m),(Support C))) /. i) . 0))
by A11, A10, A8, FINSEQ_3:25, A7;
then A19:
(C * (SgmX ((BagOrder m),(Support C)))) /. i = (P * S) /. i
by A16, A17, Def12;
A20:
Cy /. i = ((C * (SgmX ((BagOrder m),(Support C)))) /. i) * (eval (((SgmX ((BagOrder m),(Support C))) /. i),xfL))
by A12, A4, A11, A10, A3, A6, A8;
A21:
y /. i = ((P * S) /. i) * (eval ((S /. i),cxfL))
by A9, A11;
set Si =
SgmX (
(RelIncl m),
(support (S /. i)));
consider a being
FinSequence of the
carrier of
L such that A22:
(
len a = len (SgmX ((RelIncl m),(support (S /. i)))) &
eval (
(S /. i),
cxfL)
= Product a )
and A23:
for
j being
Element of
NAT st 1
<= j &
j <= len a holds
a /. j = (power L) . (
((cxfL * (SgmX ((RelIncl m),(support (S /. i))))) /. j),
(((S /. i) * (SgmX ((RelIncl m),(support (S /. i))))) /. j))
by POLYNOM2:def 2;
support (S /. i) = support ((SgmX ((BagOrder m),(Support C))) /. i)
by A16, A18, Th21;
then consider Ca being
FinSequence of the
carrier of
L such that A24:
(
len Ca = len (SgmX ((RelIncl m),(support (S /. i)))) &
eval (
((SgmX ((BagOrder m),(Support C))) /. i),
xfL)
= Product Ca )
and A25:
for
j being
Element of
NAT st 1
<= j &
j <= len Ca holds
Ca /. j = (power L) . (
((xfL * (SgmX ((RelIncl m),(support (S /. i))))) /. j),
((((SgmX ((BagOrder m),(Support C))) /. i) * (SgmX ((RelIncl m),(support (S /. i))))) /. j))
by POLYNOM2:def 2;
RelIncl m linearly_orders support (S /. i)
by PRE_POLY:82;
then A26:
rng (SgmX ((RelIncl m),(support (S /. i)))) = support (S /. i)
by PRE_POLY:def 2;
(
rng (SgmX ((RelIncl m),(support (S /. i)))) c= m &
m = dom (S /. i) &
m = dom ((SgmX ((BagOrder m),(Support C))) /. i) )
by A26, PARTFUN1:def 2;
then A27:
(
dom (((SgmX ((BagOrder m),(Support C))) /. i) * (SgmX ((RelIncl m),(support (S /. i))))) = dom (SgmX ((RelIncl m),(support (S /. i)))) &
dom (SgmX ((RelIncl m),(support (S /. i)))) = dom ((S /. i) * (SgmX ((RelIncl m),(support (S /. i))))) )
by RELAT_1:27;
(
dom xfL = m &
m = dom cxfL )
by FUNCT_2:def 1;
then A28:
(
dom (xfL * (SgmX ((RelIncl m),(support (S /. i))))) = dom (SgmX ((RelIncl m),(support (S /. i)))) &
dom (SgmX ((RelIncl m),(support (S /. i)))) = dom (cxfL * (SgmX ((RelIncl m),(support (S /. i))))) )
by A26, RELAT_1:27;
for
j being
Nat st 1
<= j &
j <= len a holds
a . j = Ca . j
proof
let j be
Nat;
( 1 <= j & j <= len a implies a . j = Ca . j )
assume A29:
( 1
<= j &
j <= len a )
;
a . j = Ca . j
A30:
j in NAT
by ORDINAL1:def 12;
A31:
(
j in dom (SgmX ((RelIncl m),(support (S /. i)))) &
j in dom a &
j in dom Ca )
by A29, A22, A24, FINSEQ_3:25;
then A32:
(
a . j = a /. j &
Ca . j = Ca /. j )
by PARTFUN1:def 6;
A33:
(
(cxfL * (SgmX ((RelIncl m),(support (S /. i))))) /. j = (cxfL * (SgmX ((RelIncl m),(support (S /. i))))) . j &
(cxfL * (SgmX ((RelIncl m),(support (S /. i))))) . j = cxfL . ((SgmX ((RelIncl m),(support (S /. i)))) . j) &
(SgmX ((RelIncl m),(support (S /. i)))) . j = (SgmX ((RelIncl m),(support (S /. i)))) /. j )
by A29, A22, FINSEQ_3:25, A28, PARTFUN1:def 6, FUNCT_1:12;
A34:
(
((S /. i) * (SgmX ((RelIncl m),(support (S /. i))))) /. j = ((S /. i) * (SgmX ((RelIncl m),(support (S /. i))))) . j &
((S /. i) * (SgmX ((RelIncl m),(support (S /. i))))) . j = (S /. i) . ((SgmX ((RelIncl m),(support (S /. i)))) . j) )
by A27, A29, A22, FINSEQ_3:25, PARTFUN1:def 6, FUNCT_1:12;
A35:
(
(xfL * (SgmX ((RelIncl m),(support (S /. i))))) /. j = (xfL * (SgmX ((RelIncl m),(support (S /. i))))) . j &
(xfL * (SgmX ((RelIncl m),(support (S /. i))))) . j = xfL . ((SgmX ((RelIncl m),(support (S /. i)))) . j) )
by A28, A29, A22, FINSEQ_3:25, PARTFUN1:def 6, FUNCT_1:12;
A36:
(
(((SgmX ((BagOrder m),(Support C))) /. i) * (SgmX ((RelIncl m),(support (S /. i))))) /. j = (((SgmX ((BagOrder m),(Support C))) /. i) * (SgmX ((RelIncl m),(support (S /. i))))) . j &
(((SgmX ((BagOrder m),(Support C))) /. i) * (SgmX ((RelIncl m),(support (S /. i))))) . j = ((SgmX ((BagOrder m),(Support C))) /. i) . ((SgmX ((RelIncl m),(support (S /. i)))) . j) )
by A27, A29, A22, FINSEQ_3:25, PARTFUN1:def 6, FUNCT_1:12;
A37:
(SgmX ((RelIncl m),(support (S /. i)))) . j in rng (SgmX ((RelIncl m),(support (S /. i))))
by A31, FUNCT_1:def 3;
then A38:
(
(SgmX ((RelIncl m),(support (S /. i)))) . j in m &
m = Segm m )
by A26;
then reconsider Sij =
(SgmX ((RelIncl m),(support (S /. i)))) . j as
Nat ;
A39:
Sij < m
by A38, NAT_1:44;
A40:
(
len f = len (FS2XFS f) &
len (FS2XFS f) = m &
m = len (FS2XFS (_sqrt f)) &
len (FS2XFS (_sqrt f)) = len (_sqrt f) )
by A1, AFINSQ_1:def 8, FUNCT_2:def 1;
A41:
xfL . Sij = f . (Sij + 1)
by A1, A40, A38, NAT_1:44, AFINSQ_1:def 8;
A42:
cxfL . Sij = (_sqrt f) . (Sij + 1)
by A1, A40, A38, NAT_1:44, AFINSQ_1:def 8;
A43:
Ca /. j = (power L) . (
((xfL * (SgmX ((RelIncl m),(support (S /. i))))) /. j),
((((SgmX ((BagOrder m),(Support C))) /. i) * (SgmX ((RelIncl m),(support (S /. i))))) /. j))
by A30, A22, A24, A25, A29;
A44:
dom (2 (#) ((SgmX ((BagOrder m),(Support C))) /. i)) = m
by PARTFUN1:def 2;
( 1
<= Sij + 1 &
Sij + 1
<= m )
by A39, NAT_1:11, NAT_1:13;
then A45:
Sij + 1
in dom f
by A40, FINSEQ_3:25;
per cases
( Sij = 0 or Sij <> 0 )
;
suppose A46:
Sij = 0
;
a . j = Ca . jthen A47:
(cxfL * (SgmX ((RelIncl m),(support (S /. i))))) /. j = (xfL * (SgmX ((RelIncl m),(support (S /. i))))) /. j
by A41, A42, A33, A35, Def11;
((S /. i) * (SgmX ((RelIncl m),(support (S /. i))))) /. j =
((2 (#) ((SgmX ((BagOrder m),(Support C))) /. i)) +* (0,(((SgmX ((BagOrder m),(Support C))) /. i) . 0))) . Sij
by A14, A11, A10, A8, FINSEQ_3:25, PARTFUN1:def 6, A18, A34
.=
(((SgmX ((BagOrder m),(Support C))) /. i) * (SgmX ((RelIncl m),(support (S /. i))))) /. j
by A36, A46, A37, A26, A44, FUNCT_7:31
;
hence
a . j = Ca . j
by A47, A32, A30, A23, A29, A43;
verum end; suppose A48:
Sij <> 0
;
a . j = Ca . jthen
Sij + 1
<> 1
;
then
(
((_sqrt f) . (Sij + 1)) * ((_sqrt f) . (Sij + 1)) = ((_sqrt f) . (Sij + 1)) ^2 &
((_sqrt f) . (Sij + 1)) ^2 = f . (Sij + 1) )
by A45, Def11, SQUARE_1:def 1;
then A49:
multcomplex . (
((_sqrt f) . (Sij + 1)),
((_sqrt f) . (Sij + 1)))
= f . (Sij + 1)
by BINOP_2:def 5;
((S /. i) * (SgmX ((RelIncl m),(support (S /. i))))) /. j =
((2 (#) ((SgmX ((BagOrder m),(Support C))) /. i)) +* (0,(((SgmX ((BagOrder m),(Support C))) /. i) . 0))) . Sij
by A14, A11, A10, A8, FINSEQ_3:25, PARTFUN1:def 6, A18, A34
.=
(2 (#) ((SgmX ((BagOrder m),(Support C))) /. i)) . Sij
by A48, FUNCT_7:32
.=
2
* ((((SgmX ((BagOrder m),(Support C))) /. i) * (SgmX ((RelIncl m),(support (S /. i))))) /. j)
by A36, VALUED_1:6
;
hence a . j =
(power L) . (
((cxfL * (SgmX ((RelIncl m),(support (S /. i))))) /. j),
(((((SgmX ((BagOrder m),(Support C))) /. i) * (SgmX ((RelIncl m),(support (S /. i))))) /. j) + ((((SgmX ((BagOrder m),(Support C))) /. i) * (SgmX ((RelIncl m),(support (S /. i))))) /. j)))
by A32, A30, A23, A29
.=
((power L) . (((cxfL * (SgmX ((RelIncl m),(support (S /. i))))) /. j),((((SgmX ((BagOrder m),(Support C))) /. i) * (SgmX ((RelIncl m),(support (S /. i))))) /. j))) * ((power L) . (((cxfL * (SgmX ((RelIncl m),(support (S /. i))))) /. j),((((SgmX ((BagOrder m),(Support C))) /. i) * (SgmX ((RelIncl m),(support (S /. i))))) /. j)))
by HURWITZ:3
.=
(power L) . (
(((cxfL * (SgmX ((RelIncl m),(support (S /. i))))) /. j) * ((cxfL * (SgmX ((RelIncl m),(support (S /. i))))) /. j)),
((((SgmX ((BagOrder m),(Support C))) /. i) * (SgmX ((RelIncl m),(support (S /. i))))) /. j))
by GROUP_1:52
.=
(power L) . (
((xfL * (SgmX ((RelIncl m),(support (S /. i))))) /. j),
((((SgmX ((BagOrder m),(Support C))) /. i) * (SgmX ((RelIncl m),(support (S /. i))))) /. j))
by A49, A41, A42, A33, A35, COMPLFLD:def 1
.=
Ca . j
by A32, A30, A22, A24, A25, A29
;
verum end;
end;
then
(
Cy /. i = y /. i &
y /. i = y . i )
by A19, A20, A21, A15, PARTFUN1:def 6, A22, A24, FINSEQ_1:14;
hence
y . i = Cy . i
by A15, PARTFUN1:def 6;
verum
end;
hence
eval (p,cxf) = eval ((JsqrtSeries p),xf)
by A8, A3, A6, FINSEQ_4:62, FINSEQ_1:14; verum