let k be Nat; :: thesis: for r being Real holds powersFS ((- (k + 1)),r,(2 * (k + 1))) = (<*((- k) to_power r)*> ^ (powersFS ((- k),r,(2 * k)))) ^ <*((k + 1) to_power r)*>
let r be Real; :: thesis: powersFS ((- (k + 1)),r,(2 * (k + 1))) = (<*((- k) to_power r)*> ^ (powersFS ((- k),r,(2 * k)))) ^ <*((k + 1) to_power r)*>
set F = powersFS ((- (k + 1)),r,(2 * (k + 1)));
set f = powersFS ((- k),r,(2 * k));
set g = <*((- k) to_power r)*>;
set h = <*((k + 1) to_power r)*>;
A1: len (powersFS ((- (k + 1)),r,(2 * (k + 1)))) = 2 * (k + 1) by Def7;
A2: len <*((- k) to_power r)*> = 1 by FINSEQ_1:39;
A3: len (powersFS ((- k),r,(2 * k))) = 2 * k by Def7;
A4: len <*((k + 1) to_power r)*> = 1 by FINSEQ_1:39;
A5: len (<*((- k) to_power r)*> ^ (powersFS ((- k),r,(2 * k)))) = (len <*((- k) to_power r)*>) + (len (powersFS ((- k),r,(2 * k)))) by FINSEQ_1:22;
then len ((<*((- k) to_power r)*> ^ (powersFS ((- k),r,(2 * k)))) ^ <*((k + 1) to_power r)*>) = ((len <*((- k) to_power r)*>) + (len (powersFS ((- k),r,(2 * k))))) + (len <*((k + 1) to_power r)*>) by FINSEQ_1:22;
hence len (powersFS ((- (k + 1)),r,(2 * (k + 1)))) = len ((<*((- k) to_power r)*> ^ (powersFS ((- k),r,(2 * k)))) ^ <*((k + 1) to_power r)*>) by A2, A3, A4, Def7; :: according to FINSEQ_1:def 18 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len (powersFS ((- (k + 1)),r,(2 * (k + 1)))) or (powersFS ((- (k + 1)),r,(2 * (k + 1)))) . b₁ = ((<*((- k) to_power r)*> ^ (powersFS ((- k),r,(2 * k)))) ^ <*((k + 1) to_power r)*>) . b₁ )
let a be Nat; :: thesis: ( not 1 <= a or not a <= len (powersFS ((- (k + 1)),r,(2 * (k + 1)))) or (powersFS ((- (k + 1)),r,(2 * (k + 1)))) . a = ((<*((- k) to_power r)*> ^ (powersFS ((- k),r,(2 * k)))) ^ <*((k + 1) to_power r)*>) . a )
assume A6: ( 1 <= a & a <= len (powersFS ((- (k + 1)),r,(2 * (k + 1)))) ) ; :: thesis: (powersFS ((- (k + 1)),r,(2 * (k + 1)))) . a = ((<*((- k) to_power r)*> ^ (powersFS ((- k),r,(2 * k)))) ^ <*((k + 1) to_power r)*>) . a
A7: (powersFS ((- (k + 1)),r,(2 * (k + 1)))) . a = ((- (k + 1)) + a) to_power r by A1, A6, Def7;

per cases ( a = 1 or ( 1 < a & a < len (powersFS ((- (k + 1)),r,(2 * (k + 1)))) ) or a = len (powersFS ((- (k + 1)),r,(2 * (k + 1)))) ) by A6, XXREAL_0:1;

suppose a = 1 ; :: thesis: (powersFS ((- (k + 1)),r,(2 * (k + 1)))) . a = ((<*((- k) to_power r)*> ^ (powersFS ((- k),r,(2 * k)))) ^ <*((k + 1) to_power r)*>) . a

hence (powersFS ((- (k + 1)),r,(2 * (k + 1)))) . a = (<*((- k) to_power r)*> ^ ((powersFS ((- k),r,(2 * k))) ^ <*((k + 1) to_power r)*>)) . a by A7
.= ((<*((- k) to_power r)*> ^ (powersFS ((- k),r,(2 * k)))) ^ <*((k + 1) to_power r)*>) . a by FINSEQ_1:32 ;
:: thesis: verum

end;

suppose that A8: 1 < a and
A9: a < len (powersFS ((- (k + 1)),r,(2 * (k + 1)))) ; :: thesis: (powersFS ((- (k + 1)),r,(2 * (k + 1)))) . a = ((<*((- k) to_power r)*> ^ (powersFS ((- k),r,(2 * k)))) ^ <*((k + 1) to_power r)*>) . a

a < ((len <*((- k) to_power r)*>) + (len (powersFS ((- k),r,(2 * k))))) + 1 by A2, A3, A9, Def7;
then A10: a <= (len <*((- k) to_power r)*>) + (len (powersFS ((- k),r,(2 * k)))) by NAT_1:13;
then A11: a in dom (<*((- k) to_power r)*> ^ (powersFS ((- k),r,(2 * k)))) by A5, A8, FINSEQ_3:25;
A12: (len <*((- k) to_power r)*>) + 1 <= a by A2, A8, NAT_1:13;
A13: 1 <= a - 1 by A8, INT_1:52;
A14: a - 1 <= (1 + (len (powersFS ((- k),r,(2 * k))))) - 1 by A2, A10, XREAL_1:9;
thus (powersFS ((- (k + 1)),r,(2 * (k + 1)))) . a = ((- k) + (a - 1)) to_power r by A7
.= (powersFS ((- k),r,(2 * k))) . (a - 1) by A3, A8, A13, A14, Def7
.= (<*((- k) to_power r)*> ^ (powersFS ((- k),r,(2 * k)))) . a by A2, A10, A12, FINSEQ_1:23
.= ((<*((- k) to_power r)*> ^ (powersFS ((- k),r,(2 * k)))) ^ <*((k + 1) to_power r)*>) . a by A11, FINSEQ_1:def 7 ; :: thesis: verum

end;

suppose A15: a = len (powersFS ((- (k + 1)),r,(2 * (k + 1)))) ; :: thesis: (powersFS ((- (k + 1)),r,(2 * (k + 1)))) . a = ((<*((- k) to_power r)*> ^ (powersFS ((- k),r,(2 * k)))) ^ <*((k + 1) to_power r)*>) . a

then a = (len (<*((- k) to_power r)*> ^ (powersFS ((- k),r,(2 * k))))) + 1 by A2, A3, A5, Def7;
hence ((<*((- k) to_power r)*> ^ (powersFS ((- k),r,(2 * k)))) ^ <*((k + 1) to_power r)*>) . a = (powersFS ((- (k + 1)),r,(2 * (k + 1)))) . a by A1, A7, A15; :: thesis: verum

end;

end;