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 ;

.= ((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_{1}[ 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_{1}[ 0 ]
by A7;

S_{1}[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

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

B3: F . 1 =
((npoly (R,n)) . (1 -' 1)) * ((power R) . (x,(1 -' 1)))
by A5, C, D, FINSEQ_1:1
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;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

.= ((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

IA: S

IS: now :: thesis: for j being Element of NAT st 0 <= j & j < len F & S_{1}[j] holds

S_{1}[j + 1]

I:
for j being Element of NAT st 0 <= j & j <= len F holds S

let j be Element of NAT ; :: thesis: ( 0 <= j & j < len F & S_{1}[j] implies S_{1}[b_{1} + 1] )

assume C1: ( 0 <= j & j < len F ) ; :: thesis: ( S_{1}[j] implies S_{1}[b_{1} + 1] )

assume C2: S_{1}[j]
; :: thesis: S_{1}[b_{1} + 1]

end;assume C1: ( 0 <= j & j < len F ) ; :: thesis: ( S

assume C2: S

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 ) )
;

end;

suppose D1:
( j = 0 & j < (len F) - 1 )
; :: thesis: S_{1}[b_{1} + 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_{1}[j + 1]
by D2; :: thesis: verum

end;.= 1. R by A7 ;

j + 1 < ((len F) - 1) + 1 by D1, XREAL_1:6;

hence S

suppose D1:
( 0 < j & j < (len F) - 1 )
; :: thesis: S_{1}[b_{1} + 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_{1}[j + 1]
by D3, B, A4, XXREAL_0:2, NAT_1:16; :: thesis: verum

end;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

suppose D1:
( 0 < j & j >= (len F) - 1 )
; :: thesis: S_{1}[b_{1} + 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_{1}[j + 1]
by D3, A4, A; :: thesis: verum

end;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

S

thus eval ((npoly (R,n)),x) = (x |^ n) + (1. R) by I, A6, A3, B4; :: thesis: verum