let R be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for n being Nat
for b being bag of n
for p1 being Polynomial of n,R
for F being FinSequence of the carrier of (Polynom-Ring (n,R)) st p1 = Sum F holds
ex g being Function of the carrier of (Polynom-Ring (n,R)), the carrier of R st
( ( for p being Polynomial of n,R holds g . p = p . b ) & p1 . b = Sum (g * F) )
let n be Nat; :: thesis: for b being bag of n
for p1 being Polynomial of n,R
for F being FinSequence of the carrier of (Polynom-Ring (n,R)) st p1 = Sum F holds
ex g being Function of the carrier of (Polynom-Ring (n,R)), the carrier of R st
( ( for p being Polynomial of n,R holds g . p = p . b ) & p1 . b = Sum (g * F) )
let b be bag of n; :: thesis: for p1 being Polynomial of n,R
for F being FinSequence of the carrier of (Polynom-Ring (n,R)) st p1 = Sum F holds
ex g being Function of the carrier of (Polynom-Ring (n,R)), the carrier of R st
( ( for p being Polynomial of n,R holds g . p = p . b ) & p1 . b = Sum (g * F) )
let p1 be Polynomial of n,R; :: thesis: for F being FinSequence of the carrier of (Polynom-Ring (n,R)) st p1 = Sum F holds
ex g being Function of the carrier of (Polynom-Ring (n,R)), the carrier of R st
( ( for p being Polynomial of n,R holds g . p = p . b ) & p1 . b = Sum (g * F) )
let F be FinSequence of the carrier of (Polynom-Ring (n,R)); :: thesis: ( p1 = Sum F implies ex g being Function of the carrier of (Polynom-Ring (n,R)), the carrier of R st
( ( for p being Polynomial of n,R holds g . p = p . b ) & p1 . b = Sum (g * F) ) )
assume A1: p1 = Sum F ; :: thesis: ex g being Function of the carrier of (Polynom-Ring (n,R)), the carrier of R st
( ( for p being Polynomial of n,R holds g . p = p . b ) & p1 . b = Sum (g * F) )
set CR = the carrier of R;
set PNR = Polynom-Ring (n,R);
set CPNR = the carrier of (Polynom-Ring (n,R));
defpred S1[ 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 :: thesis: for x being Element of the carrier of (Polynom-Ring (n,R)) ex y being Element of the carrier of R st S1[x,y]
let x be Element of the carrier of (Polynom-Ring (n,R)); :: thesis: ex y being Element of the carrier of R st S1[x,y]
reconsider x9 = x as Polynomial of n,R by POLYNOM1:def 11;
S1[x,x9 . b] ;
hence ex y being Element of the carrier of R st S1[x,y] ; :: thesis: verum
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 S1[x,g . x] from FUNCT_2:sch 3(A2);
 take g ; :: thesis: ( ( for p being Polynomial of n,R holds g . p = p . b ) & p1 . b = Sum (g * F) )
now :: thesis: for p being Polynomial of n,R holds g . p = p . b
let p be Polynomial of n,R; :: thesis: g . p = p . b
reconsider p9 = p as Element of the carrier of (Polynom-Ring (n,R)) by POLYNOM1:def 11;
S1[p9,g . p9] by A3;
hence g . p = p . b ; :: thesis: verum
end;
hence for p being Polynomial of n,R holds g . p = p . b ; :: thesis: p1 . b = Sum (g * F)
defpred S2[ Nat] means for F9 being FinSequence of the carrier of (Polynom-Ring (n,R))
for p19 being Polynomial of n,R st len F9 <= $1 & p19 = Sum F9 holds
p19 . b = Sum (g * F9);
A4: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A5: S2[k] ; :: thesis: S2[k + 1]
now :: thesis: for F9 being FinSequence of the carrier of (Polynom-Ring (n,R))
for p19 being Polynomial of n,R st len F9 <= k + 1 & p19 = Sum F9 holds
p19 . b = Sum (g * F9)
let F9 be FinSequence of the carrier of (Polynom-Ring (n,R)); :: thesis: for p19 being Polynomial of n,R st len F9 <= k + 1 & p19 = Sum F9 holds
b3 . b = Sum (g * b2)
let p19 be Polynomial of n,R; :: thesis: ( len F9 <= k + 1 & p19 = Sum F9 implies b2 . b = Sum (g * b1) )
assume that
A6: len F9 <= k + 1 and
A7: p19 = Sum F9 ; :: thesis: b2 . b = Sum (g * b1)
per cases ( len F9 < k + 1 or len F9 >= k + 1 ) ;
suppose len F9 < k + 1 ; :: thesis: b2 . b = Sum (g * b1)
then len F9 <= k by NAT_1:13;
hence p19 . b = Sum (g * F9) by A5, A7; :: thesis: verum
end;
suppose len F9 >= k + 1 ; :: thesis: b2 . b = Sum (g * b1)
then len F9 = k + 1 by A6, XXREAL_0:1;
then consider p, q being FinSequence such that
A8: len p = k and
A9: len q = 1 and
A10: F9 = p ^ q by FINSEQ_2:22;
rng q c= rng F9 by A10, FINSEQ_1:30;
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;
rng p c= rng F9 by A10, FINSEQ_1:29;
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;
A11: Sum F9 = (Sum p) + (Sum q) by A10, RLVECT_1:41;
reconsider p9 = Sum p as Polynomial of n,R by POLYNOM1:def 11;
A12: g * F9 = (g * p) ^ (g * q) by A10, FINSEQOP:9;
1 in dom q by A9, FINSEQ_3:25;
then q . 1 in rng q by FUNCT_1:def 3;
then reconsider q9 = q . 1 as Element of the carrier of (Polynom-Ring (n,R)) ;
reconsider q99 = q9 as Polynomial of n,R by POLYNOM1:def 11;
A13: q = <*q9*> by A9, FINSEQ_1:40;
then g * q = <*(g . q9)*> by FINSEQ_2:35
.= <*(q99 . b)*> by A3 ;
then A14: Sum (g * q) = q99 . b by RLVECT_1:44;
q9 = Sum q by A13, RLVECT_1:44;
then A15: p19 = p9 + q99 by A7, A11, POLYNOM1:def 11;
p9 . b = Sum (g * p) by A5, A8;
hence p19 . b = (Sum (g * p)) + (Sum (g * q)) by A14, A15, POLYNOM1:15
.= Sum (g * F9) by A12, RLVECT_1:41 ;
:: thesis: verum
end;
end;
end;
hence S2[k + 1] ; :: thesis: verum
end;
A16: S2[ 0 ]
proof
let F9 be FinSequence of the carrier of (Polynom-Ring (n,R)); :: thesis: for p19 being Polynomial of n,R st len F9 <= 0 & p19 = Sum F9 holds
p19 . b = Sum (g * F9)
let p19 be Polynomial of n,R; :: thesis: ( len F9 <= 0 & p19 = Sum F9 implies p19 . b = Sum (g * F9) )
assume that
A17: len F9 <= 0 and
A18: p19 = Sum F9 ; :: thesis: p19 . b = Sum (g * F9)
A19: F9 = <*> the carrier of (Polynom-Ring (n,R)) by A17;
then g * F9 = <*> the carrier of R ;
then A20: Sum (g * F9) = 0. R by RLVECT_1:43;
p19 = 0. (Polynom-Ring (n,R)) by A18, A19, RLVECT_1:43
.= 0_ (n,R) by POLYNOM1:def 11 ;
hence p19 . b = Sum (g * F9) by A20, POLYNOM1:22; :: thesis: verum
end;
for k being Nat holds S2[k] from NAT_1:sch 2(A16, A4);
 then S2[ len F] ;
hence p1 . b = Sum (g * F) by A1; :: thesis: verum