let m be Ordinal; :: thesis: for Pc being Polynomial of m,F_Complex
for Pr being Polynomial of m,F_Real st Pc = Pr holds
for xc being Function of m,F_Complex
for xr being Function of m,F_Real st xc = xr holds
eval (Pc,xc) = eval (Pr,xr)
let Pc be Polynomial of m,F_Complex; :: thesis: for Pr being Polynomial of m,F_Real st Pc = Pr holds
for xc being Function of m,F_Complex
for xr being Function of m,F_Real st xc = xr holds
eval (Pc,xc) = eval (Pr,xr)
let Pr be Polynomial of m,F_Real; :: thesis: ( Pc = Pr implies for xc being Function of m,F_Complex
for xr being Function of m,F_Real st xc = xr holds
eval (Pc,xc) = eval (Pr,xr) )
assume A1: Pc = Pr ; :: thesis: for xc being Function of m,F_Complex
for xr being Function of m,F_Real st xc = xr holds
eval (Pc,xc) = eval (Pr,xr)
let xc be Function of m,F_Complex; :: thesis: for xr being Function of m,F_Real st xc = xr holds
eval (Pc,xc) = eval (Pr,xr)
let xr be Function of m,F_Real; :: thesis: ( xc = xr implies eval (Pc,xc) = eval (Pr,xr) )
assume A2: xc = xr ; :: thesis: eval (Pc,xc) = eval (Pr,xr)
reconsider FC = F_Complex , FR = F_Real as Field ;
reconsider Pc = Pc as Polynomial of m,FC ;
reconsider Pr = Pr as Polynomial of m,FR ;
reconsider xc = xc as Function of m,FC ;
reconsider xr = xr as Function of m,FR ;
set S = SgmX ((BagOrder m),(Support Pc));
consider Cy being FinSequence of the carrier of FC such that
A3: ( len Cy = len (SgmX ((BagOrder m),(Support Pc))) & eval (Pc,xc) = Sum Cy ) and
A4: for i being Element of NAT st 1 <= i & i <= len Cy holds
Cy /. i = ((Pc * (SgmX ((BagOrder m),(Support Pc)))) /. i) * (eval (((SgmX ((BagOrder m),(Support Pc))) /. i),xc)) by POLYNOM2:def 4;
A5: 0. FC = 0. FR by COMPLFLD:def 1;
A6: Support Pc c= Support Pr

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Support Pc or x in Support Pr )
assume x in Support Pc ; :: thesis: x in Support Pr
then ( x in dom Pc & Pc . x <> 0. FC ) by POLYNOM1:def 3;
hence x in Support Pr by A5, A1, POLYNOM1:def 3; :: thesis: verum

end;

Support Pr c= Support Pc

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Support Pr or x in Support Pc )
assume x in Support Pr ; :: thesis: x in Support Pc
then ( x in dom Pr & Pr . x <> 0. FR ) by POLYNOM1:def 3;
hence x in Support Pc by A5, A1, POLYNOM1:def 3; :: thesis: verum

end;

then A7: Support Pr = Support Pc by A6, XBOOLE_0:def 10;
then consider Ry being FinSequence of the carrier of FR such that
A8: ( len Ry = len (SgmX ((BagOrder m),(Support Pc))) & eval (Pr,xr) = Sum Ry ) and
A9: for i being Element of NAT st 1 <= i & i <= len Ry holds
Ry /. i = ((Pr * (SgmX ((BagOrder m),(Support Pc)))) /. i) * (eval (((SgmX ((BagOrder m),(Support Pc))) /. i),xr)) by POLYNOM2:def 4;
defpred S₁[ Nat] means for i being Nat st i = $1 & $1 <= len (SgmX ((BagOrder m),(Support Pc))) holds
Sum (Ry | i) = Sum (Cy | i);
A10: S₁[ 0 ]

proof

let i be Nat; :: thesis: ( i = 0 & 0 <= len (SgmX ((BagOrder m),(Support Pc))) implies Sum (Ry | i) = Sum (Cy | i) )
assume A11: ( i = 0 & 0 <= len (SgmX ((BagOrder m),(Support Pc))) ) ; :: thesis: Sum (Ry | i) = Sum (Cy | i)
( Ry | 0 = <*> the carrier of FR & Cy | 0 = <*> the carrier of FC ) ;
then ( Sum (Ry | i) = 0. FR & Sum (Cy | i) = 0. FC ) by A11, RLVECT_1:43;
hence Sum (Ry | i) = Sum (Cy | i) by COMPLFLD:def 1; :: thesis: verum

end;

A12: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A13: S₁[n] ; :: thesis: S₁[n + 1]
let n1 be Nat; :: thesis: ( n1 = n + 1 & n + 1 <= len (SgmX ((BagOrder m),(Support Pc))) implies Sum (Ry | n1) = Sum (Cy | n1) )
assume A14: ( n1 = n + 1 & n + 1 <= len (SgmX ((BagOrder m),(Support Pc))) ) ; :: thesis: Sum (Ry | n1) = Sum (Cy | n1)
n < len (SgmX ((BagOrder m),(Support Pc))) by A14, NAT_1:13;
then A15: Sum (Ry | n) = Sum (Cy | n) by A13;
reconsider s1 = Sum (Ry | n), s2 = Ry /. n1 as Real ;
Ry | n1 = (Ry | n) ^ <*(Ry /. n1)*> by A14, A8, FINSEQ_5:82;
then Sum (Ry | n1) = (Sum (Ry | n)) + (Sum <*(Ry /. n1)*>) by RLVECT_1:41;
then A16: Sum (Ry | n1) = the addF of FR . ((Sum (Ry | n)),(Ry /. n1)) by RLVECT_1:44
.= s1 + s2 by BINOP_2:def 9 ;
Cy | n1 = (Cy | n) ^ <*(Cy /. n1)*> by A14, A3, FINSEQ_5:82;
then Sum (Cy | n1) = (Sum (Cy | n)) + (Sum <*(Cy /. n1)*>) by RLVECT_1:41;
then A17: Sum (Cy | n1) = (Sum (Cy | n)) + (Cy /. n1) by RLVECT_1:44
.= addcomplex . ((Sum (Cy | n)),(Cy /. n1)) by COMPLFLD:def 1 ;
BagOrder m linearly_orders Support Pr by POLYNOM2:18;
then rng (SgmX ((BagOrder m),(Support Pc))) = Support Pr by A7, PRE_POLY:def 2;
then ( rng (SgmX ((BagOrder m),(Support Pc))) c= Bags m & Bags m = dom Pr ) by FUNCT_2:def 1;
then A18: ( dom (Pr * (SgmX ((BagOrder m),(Support Pc)))) = dom (SgmX ((BagOrder m),(Support Pc))) & dom (Pc * (SgmX ((BagOrder m),(Support Pc)))) = dom (SgmX ((BagOrder m),(Support Pc))) ) by A1, RELAT_1:27;
n1 in dom (SgmX ((BagOrder m),(Support Pc))) by A14, NAT_1:11, FINSEQ_3:25;
then A19: ( (Pr * (SgmX ((BagOrder m),(Support Pc)))) /. n1 = (Pr * (SgmX ((BagOrder m),(Support Pc)))) . n1 & (Pr * (SgmX ((BagOrder m),(Support Pc)))) . n1 = (Pc * (SgmX ((BagOrder m),(Support Pc)))) /. n1 ) by A1, A18, PARTFUN1:def 6;
reconsider r1 = (Pr * (SgmX ((BagOrder m),(Support Pc)))) /. n1, r2 = eval (((SgmX ((BagOrder m),(Support Pc))) /. n1),xr) as Real ;
Ry /. n1 = ((Pr * (SgmX ((BagOrder m),(Support Pc)))) /. n1) * (eval (((SgmX ((BagOrder m),(Support Pc))) /. n1),xr)) by A9, A14, A8, NAT_1:11
.= r1 * r2 by BINOP_2:def 11
.= multcomplex . (r1,r2) by BINOP_2:def 5
.= the multF of FC . (r1,r2) by COMPLFLD:def 1
.= ((Pc * (SgmX ((BagOrder m),(Support Pc)))) /. n1) * (eval (((SgmX ((BagOrder m),(Support Pc))) /. n1),xc)) by A2, Th68, A19
.= Cy /. n1 by A14, NAT_1:11, A3, A4 ;
hence Sum (Ry | n1) = Sum (Cy | n1) by A15, A16, A17, BINOP_2:def 3; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A10, A12);
then Sum (Ry | (len (SgmX ((BagOrder m),(Support Pc))))) = Sum (Cy | (len (SgmX ((BagOrder m),(Support Pc))))) ;
hence eval (Pc,xc) = eval (Pr,xr) by A3, A8; :: thesis: verum