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 ;
then A5: ( len r in dom r & (len r) -' 1 = (len r) - 1 & (n + 1) -' (len r) = 0 ) by ;
then A6: ( r . (len r) = (p . n) * (<%z%> . ((n + 1) -' (len r))) & <%z%> . ((n + 1) -' (len r)) = z ) by ;
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 ;
k <= len r by ;
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 ;
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 ;
hence (p *' <%z%>) . n = (p . n) * z by ; :: thesis: verum