let R be non empty doubleLoopStr ; :: thesis: for x being Scalar of R
for f being FinSequence of R st f is being_a_generation_from_squares & x is being_a_square holds
(f ^ <*x*>) ^ <*((f /. (len f)) + x)*> is being_a_generation_from_squares
let x be Scalar of R; :: thesis: for f being FinSequence of R st f is being_a_generation_from_squares & x is being_a_square holds
(f ^ <*x*>) ^ <*((f /. (len f)) + x)*> is being_a_generation_from_squares
let f be FinSequence of R; :: thesis: ( f is being_a_generation_from_squares & x is being_a_square implies (f ^ <*x*>) ^ <*((f /. (len f)) + x)*> is being_a_generation_from_squares )
assume A1: ( f is being_a_generation_from_squares & x is being_a_square ) ; :: thesis: (f ^ <*x*>) ^ <*((f /. (len f)) + x)*> is being_a_generation_from_squares
then A2: f ^ <*x*> is being_a_generation_from_squares by Lm34;
A3: len <*x*> = 1 by Lm2;
A4: len f <> 0 by A1, Def14;
A5: len f <= (len f) + 1 by NAT_1:11;
A6: ( (len f) + 1 <> 0 & (len f) + 1 = len (f ^ <*x*>) ) by A3, FINSEQ_1:35, NAT_1:5;
A7: (f ^ <*x*>) /. (len f) = f /. (len f) by A4, Lm4;
(f ^ <*x*>) /. ((len f) + 1) = x by Lm3;
hence (f ^ <*x*>) ^ <*((f /. (len f)) + x)*> is being_a_generation_from_squares by A2, A4, A5, A6, A7, Lm32; :: thesis: verum