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

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

hence (powersFS ((- (k + 1)),r,((2 * (k + 1)) - 1))) . a = (<*((- k) to_power r)*> ^ ((powersFS ((- k),r,((2 * k) - 1))) ^ <*(k to_power r)*>)) . a by A7
.= ((<*((- k) to_power r)*> ^ (powersFS ((- k),r,((2 * k) - 1)))) ^ <*(k 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)) - 1))) ; :: thesis: (powersFS ((- (k + 1)),r,((2 * (k + 1)) - 1))) . a = ((<*((- k) to_power r)*> ^ (powersFS ((- k),r,((2 * k) - 1)))) ^ <*(k to_power r)*>) . a

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

end;

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

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

end;

end;