let R be non empty doubleLoopStr ; :: thesis: for x being Scalar of R
for f being FinSequence of R st f is being_a_Sum_of_products_of_squares & x is being_a_product_of_squares holds
f ^ <*((f /. (len f)) + x)*> is being_a_Sum_of_products_of_squares
let x be Scalar of R; :: thesis: for f being FinSequence of R st f is being_a_Sum_of_products_of_squares & x is being_a_product_of_squares holds
f ^ <*((f /. (len f)) + x)*> is being_a_Sum_of_products_of_squares
let f be FinSequence of R; :: thesis: ( f is being_a_Sum_of_products_of_squares & x is being_a_product_of_squares implies f ^ <*((f /. (len f)) + x)*> is being_a_Sum_of_products_of_squares )
assume that
A1: f is being_a_Sum_of_products_of_squares and
A2: x is being_a_product_of_squares ; :: thesis: f ^ <*((f /. (len f)) + x)*> is being_a_Sum_of_products_of_squares
set g = f ^ <*((f /. (len f)) + x)*>;
A3: len (f ^ <*((f /. (len f)) + x)*>) = (len f) + (len <*((f /. (len f)) + x)*>) by FINSEQ_1:22
.= (len f) + 1 by Lm2 ;
A4: for n being Nat st n <> 0 & n < len (f ^ <*((f /. (len f)) + x)*>) holds
f /. n = (f ^ <*((f /. (len f)) + x)*>) /. n
proof
let n be Nat; :: thesis: ( n <> 0 & n < len (f ^ <*((f /. (len f)) + x)*>) implies f /. n = (f ^ <*((f /. (len f)) + x)*>) /. n )
assume ( n <> 0 & n < len (f ^ <*((f /. (len f)) + x)*>) ) ; :: thesis: f /. n = (f ^ <*((f /. (len f)) + x)*>) /. n
then ( 1 <= n & n <= len f ) by A3, NAT_1:13, NAT_1:25;
then n in dom f by FINSEQ_3:25;
hence f /. n = (f ^ <*((f /. (len f)) + x)*>) /. n by Lm1; :: thesis: verum
end;
A5: for n being Nat st n <> 0 & n < len (f ^ <*((f /. (len f)) + x)*>) holds
ex y being Scalar of R st
( y is being_a_product_of_squares & (f ^ <*((f /. (len f)) + x)*>) /. (n + 1) = ((f ^ <*((f /. (len f)) + x)*>) /. n) + y )
proof
let n be Nat; :: thesis: ( n <> 0 & n < len (f ^ <*((f /. (len f)) + x)*>) implies ex y being Scalar of R st
( y is being_a_product_of_squares & (f ^ <*((f /. (len f)) + x)*>) /. (n + 1) = ((f ^ <*((f /. (len f)) + x)*>) /. n) + y ) )
assume that
A6: n <> 0 and
A7: n < len (f ^ <*((f /. (len f)) + x)*>) ; :: thesis: ex y being Scalar of R st
( y is being_a_product_of_squares & (f ^ <*((f /. (len f)) + x)*>) /. (n + 1) = ((f ^ <*((f /. (len f)) + x)*>) /. n) + y )
A8: now :: thesis: ( n < len f implies ex y being Scalar of R st
( y is being_a_product_of_squares & (f ^ <*((f /. (len f)) + x)*>) /. (n + 1) = ((f ^ <*((f /. (len f)) + x)*>) /. n) + y ) )
A9: f /. n = (f ^ <*((f /. (len f)) + x)*>) /. n by A4, A6, A7;
assume A10: n < len f ; :: thesis: ex y being Scalar of R st
( y is being_a_product_of_squares & (f ^ <*((f /. (len f)) + x)*>) /. (n + 1) = ((f ^ <*((f /. (len f)) + x)*>) /. n) + y )
then ( n + 1 <> 0 & n + 1 < len (f ^ <*((f /. (len f)) + x)*>) ) by A3, XREAL_1:6;
then f /. (n + 1) = (f ^ <*((f /. (len f)) + x)*>) /. (n + 1) by A4;
hence ex y being Scalar of R st
( y is being_a_product_of_squares & (f ^ <*((f /. (len f)) + x)*>) /. (n + 1) = ((f ^ <*((f /. (len f)) + x)*>) /. n) + y ) by A1, A6, A10, A9; :: thesis: verum
end;
A11: now :: thesis: ( n = len f implies ex y being Scalar of R st
( y is being_a_product_of_squares & (f ^ <*((f /. (len f)) + x)*>) /. (n + 1) = ((f ^ <*((f /. (len f)) + x)*>) /. n) + y ) )
assume A12: n = len f ; :: thesis: ex y being Scalar of R st
( y is being_a_product_of_squares & (f ^ <*((f /. (len f)) + x)*>) /. (n + 1) = ((f ^ <*((f /. (len f)) + x)*>) /. n) + y )
1 <= n by A6, NAT_1:25;
then A13: n in dom f by A12, FINSEQ_3:25;
(f ^ <*((f /. (len f)) + x)*>) /. (n + 1) = (f /. n) + x by A12, Lm3;
then (f ^ <*((f /. (len f)) + x)*>) /. (n + 1) = ((f ^ <*((f /. (len f)) + x)*>) /. n) + x by A13, Lm1;
hence ex y being Scalar of R st
( y is being_a_product_of_squares & (f ^ <*((f /. (len f)) + x)*>) /. (n + 1) = ((f ^ <*((f /. (len f)) + x)*>) /. n) + y ) by A2; :: thesis: verum
end;
n <= len f by A3, A7, NAT_1:13;
hence ex y being Scalar of R st
( y is being_a_product_of_squares & (f ^ <*((f /. (len f)) + x)*>) /. (n + 1) = ((f ^ <*((f /. (len f)) + x)*>) /. n) + y ) by A8, A11, XXREAL_0:1; :: thesis: verum
end;
len f <> 0 by A1;
then 1 <= len f by NAT_1:25;
then 1 < len (f ^ <*((f /. (len f)) + x)*>) by A3, NAT_1:13;
then (f ^ <*((f /. (len f)) + x)*>) /. 1 = f /. 1 by A4;
then A14: (f ^ <*((f /. (len f)) + x)*>) /. 1 is being_a_product_of_squares by A1;
len (f ^ <*((f /. (len f)) + x)*>) <> 0 by A3;
hence f ^ <*((f /. (len f)) + x)*> is being_a_Sum_of_products_of_squares by A14, A5; :: thesis: verum