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 that
A1: f is being_a_generation_from_squares and
A2: x is being_a_square ; :: thesis: (f ^ <*x*>) ^ <*((f /. (len f)) * x)*> is being_a_generation_from_squares
A3: f ^ <*x*> is being_a_generation_from_squares by A1, A2, Lm34;
len <*x*> = 1 by Lm2;
then A4: (len f) + 1 = len (f ^ <*x*>) by FINSEQ_1:22;
A5: ( len f <= (len f) + 1 & (len f) + 1 <> 0 ) by NAT_1:11;
A6: (f ^ <*x*>) /. ((len f) + 1) = x by Lm3;
A7: len f <> 0 by A1;
then (f ^ <*x*>) /. (len f) = f /. (len f) by Lm4;
hence (f ^ <*x*>) ^ <*((f /. (len f)) * x)*> is being_a_generation_from_squares by A3, A7, A5, A4, A6, Lm45; :: thesis: verum