let n be Nat; for L being non empty right_complementable add-associative right_zeroed distributive unital doubleLoopStr
for x, y being Element of L holds eval ((seq (n,x)),y) = ((seq (n,x)) . n) * (power (y,n))
let L be non empty right_complementable add-associative right_zeroed distributive unital doubleLoopStr ; for x, y being Element of L holds eval ((seq (n,x)),y) = ((seq (n,x)) . n) * (power (y,n))
let x, y be Element of L; eval ((seq (n,x)),y) = ((seq (n,x)) . n) * (power (y,n))
set p = seq (n,x);
consider F being FinSequence of L such that
A1:
eval ((seq (n,x)),y) = Sum F
and
A2:
len F = len (seq (n,x))
and
A3:
for n being Element of NAT st n in dom F holds
F . n = ((seq (n,x)) . (n -' 1)) * ((power L) . (y,(n -' 1)))
by POLYNOM4:def 2;
per cases
( len (seq (n,x)) > 0 or len (seq (n,x)) = 0 )
;
suppose A4:
len (seq (n,x)) > 0
;
eval ((seq (n,x)),y) = ((seq (n,x)) . n) * (power (y,n))then A5:
len (seq (n,x)) >= 0 + 1
by NAT_1:13;
then A6:
len (seq (n,x)) in dom F
by A2, FINSEQ_3:25;
seq (
n,
x)
<> 0_. L
by A4, POLYNOM4:3;
then
x <> 0. L
by Th28;
then A7:
len (seq (n,x)) = n + 1
by Th27;
A8:
(n + 1) -' 1
= n
by NAT_D:34;
hence eval (
(seq (n,x)),
y) =
F /. (n + 1)
by A1, A7, A5, A2, FINSEQ_3:25, POLYNOM2:3
.=
F . (n + 1)
by A7, A6, PARTFUN1:def 6
.=
((seq (n,x)) . n) * (power (y,n))
by A3, A7, A5, A8, A2, FINSEQ_3:25
;
verum end; end;