let R be non degenerated Ring; :: thesis: for n being non zero Nat
for x being Element of R holds eval ((npoly (R,n)),x) = (x |^ n) + (1. R)
let n be non zero Nat; :: thesis: for x being Element of R holds eval ((npoly (R,n)),x) = (x |^ n) + (1. R)
let x be Element of R; :: thesis: eval ((npoly (R,n)),x) = (x |^ n) + (1. R)
set q = npoly (R,n);
consider F being FinSequence of R such that
A3: eval ((npoly (R,n)),x) = Sum F and
A4: len F = len (npoly (R,n)) and
A5: for j being Element of NAT st j in dom F holds
F . j = ((npoly (R,n)) . (j -' 1)) * ((power R) . (x,(j -' 1))) by POLYNOM4:def 2;
A: n = deg (npoly (R,n)) by lem6
.= (len (npoly (R,n))) - 1 by HURWITZ:def 2 ;
then B: len (npoly (R,n)) = n + 1 ;
C: dom F = Seg (n + 1) by A, A4, FINSEQ_1:def 3;
D: 1 <= n + 1 by NAT_1:11;
E: (n + 1) -' 1 = (n + 1) - 1 by NAT_1:11, XREAL_1:233;
B1: F . (n + 1) = ((npoly (R,n)) . n) * ((power R) . (x,((n + 1) -' 1))) by E, A5, D, C, FINSEQ_1:1
.= (1. R) * ((power R) . (x,((n + 1) -' 1))) by Lm10
.= x |^ n by E ;

B2: now :: thesis: for j being Element of NAT st 1 < j & j <= n holds
F . j = 0. R

let j be Element of NAT ; :: thesis: ( 1 < j & j <= n implies F . j = 0. R )
assume H0: ( 1 < j & j <= n ) ; :: thesis: F . j = 0. R
reconsider j1 = j -' 1 as Element of NAT ;
reconsider n1 = n - 1 as Element of NAT by INT_1:3;
n <= n + 1 by NAT_1:11;
then H1: j <= n + 1 by H0, XXREAL_0:2;
H4: j1 = j - 1 by H0, XREAL_1:233;
then H2: j1 <> 0 by H0;
j1 + 1 <= n1 + 1 by H4, H0;
then H3: j1 <> n by NAT_1:13;
thus F . j = ((npoly (R,n)) . j1) * ((power R) . (x,(j -' 1))) by A5, H1, C, H0, FINSEQ_1:1
.= (0. R) * ((power R) . (x,(j -' 1))) by H2, H3, Lm11
.= 0. R ; :: thesis: verum

end;

B3: F . 1 = ((npoly (R,n)) . (1 -' 1)) * ((power R) . (x,(1 -' 1))) by A5, C, D, FINSEQ_1:1
.= ((npoly (R,n)) . 0) * ((power R) . (x,(1 -' 1))) by NAT_2:8
.= ((npoly (R,n)) . 0) * ((power R) . (x,0)) by NAT_2:8
.= (1. R) * ((power R) . (x,0)) by Lm10
.= (1. R) * (1_ R) by GROUP_1:def 7
.= 1. R ;
B4: len F <> 0 by A, A4;
consider fp being sequence of the carrier of R such that
A6: Sum F = fp . (len F) and
A7: fp . 0 = 0. R and
A8: for j being Nat
for v being Element of R st j < len F & v = F . (j + 1) holds
fp . (j + 1) = (fp . j) + v by RLVECT_1:def 12;
defpred S₁[ Element of NAT ] means ( ( $1 = 0 & fp . $1 = 0. R ) or ( 0 < $1 & $1 < len F & fp . $1 = 1. R ) or ( $1 = len F & fp . $1 = (x |^ n) + (1. R) ) );
IA: S₁[ 0 ] by A7;

IS: now :: thesis: for j being Element of NAT st 0 <= j & j < len F & S₁[j] holds
S₁[j + 1]

let j be Element of NAT ; :: thesis: ( 0 <= j & j < len F & S₁[j] implies S₁[b₁ + 1] )
assume C1: ( 0 <= j & j < len F ) ; :: thesis: ( S₁[j] implies S₁[b₁ + 1] )
assume C2: S₁[j] ; :: thesis: S₁[b₁ + 1]

per cases ( ( j = 0 & j < (len F) - 1 ) or ( j = 0 & j >= (len F) - 1 ) or ( 0 < j & j < (len F) - 1 ) or ( 0 < j & j >= (len F) - 1 ) ) ;

suppose D1: ( j = 0 & j < (len F) - 1 ) ; :: thesis: S₁[b₁ + 1]

then D2: fp . (j + 1) = (fp . 0) + (1. R) by B3, A8, C1
.= 1. R by A7 ;
j + 1 < ((len F) - 1) + 1 by D1, XREAL_1:6;
hence S₁[j + 1] by D2; :: thesis: verum

end;

suppose ( j = 0 & j >= (len F) - 1 ) ; :: thesis: S₁[b₁ + 1]

hence S₁[j + 1] by A, A4; :: thesis: verum

end;

suppose D1: ( 0 < j & j < (len F) - 1 ) ; :: thesis: S₁[b₁ + 1]

then D3: j + 1 <= n by A, A4, INT_1:7;
j + 1 > 0 + 1 by D1, XREAL_1:8;
then F . (j + 1) = 0. R by D3, B2;
then fp . (j + 1) = (1. R) + (0. R) by C2, D1, C1, A8;
hence S₁[j + 1] by D3, B, A4, XXREAL_0:2, NAT_1:16; :: thesis: verum

end;

suppose D1: ( 0 < j & j >= (len F) - 1 ) ; :: thesis: S₁[b₁ + 1]

j + 1 <= len F by INT_1:7, C1;
then (j + 1) - 1 <= (len F) - 1 by XREAL_1:9;
then D3: j = n by A4, A, D1, XXREAL_0:1;
then fp . (j + 1) = (1. R) + (x |^ n) by B1, C1, C2, A8
.= (x |^ n) + (1. R) by RLVECT_1:def 2 ;
hence S₁[j + 1] by D3, A4, A; :: thesis: verum

end;

end;

end;

I: for j being Element of NAT st 0 <= j & j <= len F holds
S₁[j] from INT_1:sch 7(IA, IS);
thus eval ((npoly (R,n)),x) = (x |^ n) + (1. R) by I, A6, A3, B4; :: thesis: verum