let n be Nat; :: thesis: 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 ; :: thesis: 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; :: thesis: 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 ; :: thesis: 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;

now :: thesis: for i being Element of NAT st i in dom F & i <> n + 1 holds
F /. i = 0. L

let i be Element of NAT ; :: thesis: ( i in dom F & i <> n + 1 implies F /. i = 0. L )
assume that
A9: i in dom F and
A10: i <> n + 1 ; :: thesis: F /. i = 0. L
i in Seg (len F) by A9, FINSEQ_1:def 3;
then i >= 0 + 1 by FINSEQ_1:1;
then i -' 1 = i - 1 by XREAL_1:19, XREAL_0:def 2;
then i -' 1 <> n by A10;
then A11: (seq (n,x)) . (i -' 1) = 0. L by Th25;
thus F /. i = F . i by A9, PARTFUN1:def 6
.= (0. L) * ((power L) . (y,(i -' 1))) by A3, A9, A11
.= 0. L ; :: thesis: verum

end;

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 ;
:: thesis: verum

end;

suppose len (seq (n,x)) = 0 ; :: thesis: eval ((seq (n,x)),y) = ((seq (n,x)) . n) * (power (y,n))

then A12: seq (n,x) = 0_. L by POLYNOM4:5;
then (seq (n,x)) . n = 0. L by ORDINAL1:def 12, FUNCOP_1:7;
hence eval ((seq (n,x)),y) = ((seq (n,x)) . n) * (power (y,n)) by A12, POLYNOM4:17; :: thesis: verum

end;

end;