let R be non empty doubleLoopStr ; :: thesis: for x, y being Scalar of R st x is generated_from_squares & y is generated_from_squares holds
x * y is generated_from_squares
let x, y be Scalar of R; :: thesis: ( x is generated_from_squares & y is generated_from_squares implies x * y is generated_from_squares )
assume that
A1: x is generated_from_squares and
A2: y is generated_from_squares ; :: thesis: x * y is generated_from_squares
consider f being FinSequence of R such that
A3: f is being_a_generation_from_squares and
A4: x = f /. (len f) by A1;
consider g being FinSequence of R such that
A5: g is being_a_generation_from_squares and
A6: y = g /. (len g) by A2;
set h = (f ^ g) ^ <*((f /. (len f)) * (g /. (len g)))*>;
len ((f ^ g) ^ <*((f /. (len f)) * (g /. (len g)))*>) = (len (f ^ g)) + (len <*((f /. (len f)) * (g /. (len g)))*>) by FINSEQ_1:22
.= (len (f ^ g)) + 1 by Lm2 ;
then A7: ((f ^ g) ^ <*((f /. (len f)) * (g /. (len g)))*>) /. (len ((f ^ g) ^ <*((f /. (len f)) * (g /. (len g)))*>)) = x * (g /. (len g)) by A4, Lm3;
(f ^ g) ^ <*((f /. (len f)) * (g /. (len g)))*> is being_a_generation_from_squares by A3, A5, Lm85;
hence x * y is generated_from_squares by A6, A7; :: thesis: verum