let R be non empty non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis:
let n be Element of NAT ; :: thesis:
let b be bag of ; :: thesis:
let p1 be Polynomial of n,R; :: thesis:
let F be FinSequence of the carrier of (Polynom-Ring n,R); :: thesis:
assume A1: p1 = Sum F ; :: thesis:
set PNR = Polynom-Ring n,R;
set CPNR = the carrier of (Polynom-Ring n,R);
set CR = the carrier of R;
defpred S₁[ Element of the carrier of (Polynom-Ring n,R), Element of the carrier of R] means for p being Polynomial of n,R st p = $1 holds
$2 = p . b;

A2: now

let x be Element of the carrier of (Polynom-Ring n,R); :: thesis:
reconsider x' = x as Polynomial of n,R by POLYNOM1:def 27;
S₁[x,x' . b] ;
hence ex y being Element of the carrier of R st S₁[x,y] ; :: thesis:

end;

consider g being Function of the carrier of (Polynom-Ring n,R),the carrier of R such that
A3: for x being Element of the carrier of (Polynom-Ring n,R) holds S₁[x,g . x] from FUNCT_2:sch 3(A2);
take g ; :: thesis:

let p be Polynomial of n,R; :: thesis:
reconsider p' = p as Element of the carrier of (Polynom-Ring n,R) by POLYNOM1:def 27;
S₁[p',g . p'] by A3;
hence g . p = p . b ; :: thesis:

end;

hence for p being Polynomial of n,R holds g . p = p . b ; :: thesis:
defpred S₂[ Nat] means for F' being FinSequence of the carrier of (Polynom-Ring n,R)
for p1' being Polynomial of n,R st len F' <= $1 & p1' = Sum F' holds
p1' . b = Sum (g * F');
A4: S₂[ 0 ]

let F' be FinSequence of the carrier of (Polynom-Ring n,R); :: thesis:
let p1' be Polynomial of n,R; :: thesis:
assume A5: ( len F' <= 0 & p1' = Sum F' ) ; :: thesis:
then len F' = 0 ;
then A6: F' = <*> the carrier of (Polynom-Ring n,R) ;
then A7: p1' = 0. (Polynom-Ring n,R) by A5, RLVECT_1:60
.= 0_ n,R by POLYNOM1:def 27 ;
g * F' = <*> the carrier of R by A6;
then Sum (g * F') = 0. R by RLVECT_1:60;
hence p1' . b = Sum (g * F') by A7, POLYNOM1:81; :: thesis:

end;

A8: for k being Element of NAT st S₂[k] holds
S₂[k + 1]

let k be Element of NAT ; :: thesis:
assume A9: S₂[k] ; :: thesis:

let F' be FinSequence of the carrier of (Polynom-Ring n,R); :: thesis:
let p1' be Polynomial of n,R; :: thesis:
assume A10: ( len F' <= k + 1 & p1' = Sum F' ) ; :: thesis:

per cases ;

suppose len F' < k + 1 ; :: thesis:

then len F' <= k by NAT_1:13;
hence p1' . b = Sum (g * F') by A9, A10; :: thesis:

end;

suppose len F' >= k + 1 ; :: thesis:

then len F' = k + 1 by A10, XXREAL_0:1;
then consider p, q being FinSequence such that
A11: ( len p = k & len q = 1 & F' = p ^ q ) by FINSEQ_2:25;
rng p c= rng F' by A11, FINSEQ_1:42;
then rng p c= the carrier of (Polynom-Ring n,R) by XBOOLE_1:1;
then reconsider p = p as FinSequence of the carrier of (Polynom-Ring n,R) by FINSEQ_1:def 4;
reconsider p' = Sum p as Polynomial of n,R by POLYNOM1:def 27;
A12: p' . b = Sum (g * p) by A9, A11;
rng q c= rng F' by A11, FINSEQ_1:43;
then rng q c= the carrier of (Polynom-Ring n,R) by XBOOLE_1:1;
then reconsider q = q as FinSequence of the carrier of (Polynom-Ring n,R) by FINSEQ_1:def 4;
1 in dom q by A11, FINSEQ_3:27;
then q . 1 in rng q by FUNCT_1:def 5;
then reconsider q' = q . 1 as Element of the carrier of (Polynom-Ring n,R) ;
A13: q = <*q'*> by A11, FINSEQ_1:57;
then A14: q' = Sum q by RLVECT_1:61;
reconsider q'' = q' as Polynomial of n,R by POLYNOM1:def 27;
g * q = <*(g . q')*> by A13, FINSEQ_2:39
.= <*(q'' . b)*> by A3 ;
then A15: Sum (g * q) = q'' . b by RLVECT_1:61;
A16: Sum F' = (Sum p) + (Sum q) by A11, RLVECT_1:58;
A17: g * F' = (g * p) ^ (g * q) by A11, FINSEQOP:10;
p1' = p' + q'' by A10, A14, A16, POLYNOM1:def 27;
hence p1' . b = (Sum (g * p)) + (Sum (g * q)) by A12, A15, POLYNOM1:def 21
.= Sum (g * F') by A17, RLVECT_1:58 ;
:: thesis:

end;

hence S₂[k + 1] ; :: thesis:

end;

for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A4, A8);
then S₂[ len F] ;
hence p1 . b = Sum (g * F) by A1; :: thesis: