let m be Ordinal; :: thesis: for b being bag of m
for xc being Function of m,F_Complex
for xr being Function of m,F_Real st xc = xr holds
eval (b,xc) = eval (b,xr)
let b be bag of m; :: thesis: for xc being Function of m,F_Complex
for xr being Function of m,F_Real st xc = xr holds
eval (b,xc) = eval (b,xr)
let xc be Function of m,F_Complex; :: thesis: for xr being Function of m,F_Real st xc = xr holds
eval (b,xc) = eval (b,xr)
let xr be Function of m,F_Real; :: thesis: ( xc = xr implies eval (b,xc) = eval (b,xr) )
assume A1: xc = xr ; :: thesis: eval (b,xc) = eval (b,xr)
reconsider FC = F_Complex , FR = F_Real as Field ;
reconsider xc = xc as Function of m,FC ;
reconsider xr = xr as Function of m,FR ;
set S = SgmX ((RelIncl m),(support b));
consider yC being FinSequence of FC such that
A2: ( len yC = len (SgmX ((RelIncl m),(support b))) & eval (b,xc) = Product yC ) and
A3: for i being Element of NAT st 1 <= i & i <= len yC holds
yC /. i = (power FC) . (((xc * (SgmX ((RelIncl m),(support b)))) /. i),((b * (SgmX ((RelIncl m),(support b)))) /. i)) by POLYNOM2:def 2;
consider yR being FinSequence of FR such that
A4: ( len yR = len (SgmX ((RelIncl m),(support b))) & eval (b,xr) = Product yR ) and
A5: for i being Element of NAT st 1 <= i & i <= len yR holds
yR /. i = (power FR) . (((xr * (SgmX ((RelIncl m),(support b)))) /. i),((b * (SgmX ((RelIncl m),(support b)))) /. i)) by POLYNOM2:def 2;
RelIncl m linearly_orders support b by PRE_POLY:82;
then A6: rng (SgmX ((RelIncl m),(support b))) = support b by PRE_POLY:def 2;
A7: ( dom xc = m & m = dom xr & m = dom b ) by PARTFUN1:def 2;
A8: ( dom (xc * (SgmX ((RelIncl m),(support b)))) = dom (SgmX ((RelIncl m),(support b))) & dom (xr * (SgmX ((RelIncl m),(support b)))) = dom (SgmX ((RelIncl m),(support b))) & dom (xr * (SgmX ((RelIncl m),(support b)))) = dom (SgmX ((RelIncl m),(support b))) ) by A6, A7, RELAT_1:27;
for i being Nat st 1 <= i & i <= len (SgmX ((RelIncl m),(support b))) holds
yC . i = yR . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len (SgmX ((RelIncl m),(support b))) implies yC . i = yR . i )
assume A9: ( 1 <= i & i <= len (SgmX ((RelIncl m),(support b))) ) ; :: thesis: yC . i = yR . i
A10: ( i in NAT & (b * (SgmX ((RelIncl m),(support b)))) /. i in NAT ) by ORDINAL1:def 12;
reconsider r = (xr * (SgmX ((RelIncl m),(support b)))) /. i as Real ;
A11: ( i in dom (SgmX ((RelIncl m),(support b))) & i in dom yR & i in dom yC ) by A9, FINSEQ_3:25, A2, A4;
A12: ( (xc * (SgmX ((RelIncl m),(support b)))) /. i = (xc * (SgmX ((RelIncl m),(support b)))) . i & (xc * (SgmX ((RelIncl m),(support b)))) . i = xc . ((SgmX ((RelIncl m),(support b))) . i) & (xr * (SgmX ((RelIncl m),(support b)))) /. i = (xr * (SgmX ((RelIncl m),(support b)))) . i & (xr * (SgmX ((RelIncl m),(support b)))) . i = xr . ((SgmX ((RelIncl m),(support b))) . i) ) by PARTFUN1:def 6, A9, FINSEQ_3:25, A8, FUNCT_1:12;
then A13: ex x being Real st
( x = (xc * (SgmX ((RelIncl m),(support b)))) /. i & (power F_Complex) . (((xc * (SgmX ((RelIncl m),(support b)))) /. i),((b * (SgmX ((RelIncl m),(support b)))) /. i)) = x |^ ((b * (SgmX ((RelIncl m),(support b)))) /. i) ) by A1, UNIROOTS:43;
thus yR . i = yR /. i by A11, PARTFUN1:def 6
.= (power FR) . (((xr * (SgmX ((RelIncl m),(support b)))) /. i),((b * (SgmX ((RelIncl m),(support b)))) /. i)) by A10, A9, A4, A5
.= (power FC) . (((xc * (SgmX ((RelIncl m),(support b)))) /. i),((b * (SgmX ((RelIncl m),(support b)))) /. i)) by NIVEN:7, A13, A12, A1
.= yC /. i by A10, A9, A2, A3
.= yC . i by A11, PARTFUN1:def 6 ; :: thesis: verum

end;

hence eval (b,xc) = eval (b,xr) by Th67, A4, A2, FINSEQ_1:14; :: thesis: verum