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

hence (p *' <%z%>) . n = (p . n) * z by A6, A2, A5, PARTFUN1:def 6; :: thesis: verum

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

then
Sum r = r /. (len r)
by A4, FINSEQ_3:25, POLYNOM2:3;
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;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

hence (p *' <%z%>) . n = (p . n) * z by A6, A2, A5, PARTFUN1:def 6; :: thesis: verum