let n be Nat; :: thesis: for L being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for z being Element of L
for p being Polynomial of L holds (p *' <%z%>) . n = (p . n) * z
let L be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ; :: thesis: for z being Element of L
for p being Polynomial of L holds (p *' <%z%>) . n = (p . n) * z
let z be Element of L; :: thesis: for p being Polynomial of L holds (p *' <%z%>) . n = (p . n) * z
let p be Polynomial of L; :: thesis: (p *' <%z%>) . n = (p . n) * z
set Z = <%z%>;
n in NAT by ORDINAL1:def 12;
then consider r being FinSequence of the carrier of L such that
A1: len r = n + 1 and
A2: (p *' <%z%>) . n = Sum r and
A3: for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (<%z%> . ((n + 1) -' k)) by POLYNOM3:def 9;
set l = len r;
A4: 1 <= len r by A1, NAT_1:11;
then A5: ( len r in dom r & (len r) -' 1 = (len r) - 1 & (n + 1) -' (len r) = 0 ) by A1, FINSEQ_3:25, XREAL_1:233, XREAL_1:232;
then A6: ( r . (len r) = (p . n) * (<%z%> . ((n + 1) -' (len r))) & <%z%> . ((n + 1) -' (len r)) = z ) by A1, A3, POLYNOM5:32;
for k being Element of NAT st k in dom r & k <> len r holds
r /. k = 0. L

proof

let k be Element of NAT ; :: thesis: ( k in dom r & k <> len r implies r /. k = 0. L )
assume A7: ( k in dom r & k <> len r ) ; :: thesis: r /. k = 0. L
A8: r /. k = r . k by PARTFUN1:def 6, A7;
k <= len r by A7, FINSEQ_3:25;
then (len r) -' k = (len r) - k by XREAL_1:233;
then (len r) -' k <> 0 by A7;
then <%z%> . ((len r) -' k) = 0. L by NAT_1:14, POLYNOM5:32;
then (p . (k -' 1)) * (<%z%> . ((len r) -' k)) = 0. L ;
hence r /. k = 0. L by A1, A8, A7, A3; :: thesis: verum

end;

then Sum r = r /. (len r) by A4, FINSEQ_3:25, POLYNOM2:3;
hence (p *' <%z%>) . n = (p . n) * z by A6, A2, A5, PARTFUN1:def 6; :: thesis: verum