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*> 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*> 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*> 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*> is being_a_generation_from_squares
<*x*> is being_a_generation_from_squares by A2, Lm30;
hence f ^ <*x*> is being_a_generation_from_squares by A1, Lm33; :: thesis: verum