let R be non empty doubleLoopStr ; :: thesis: for x, y being Scalar of R st x is being_an_amalgam_of_squares & y is being_an_amalgam_of_squares holds
x * y is being_an_amalgam_of_squares
let x, y be Scalar of R; :: thesis: ( x is being_an_amalgam_of_squares & y is being_an_amalgam_of_squares implies x * y is being_an_amalgam_of_squares )
assume that
A1: x is being_an_amalgam_of_squares and
A2: y is being_an_amalgam_of_squares ; :: thesis: x * y is being_an_amalgam_of_squares
consider f being FinSequence of R such that
A3: ( f is being_an_Amalgam_of_squares & x = f /. (len f) ) by A1;
consider g being FinSequence of R such that
A4: ( g is being_an_Amalgam_of_squares & y = g /. (len g) ) by A2;
take h = (f ^ g) ^ <*((f /. (len f)) * (g /. (len g)))*>; :: according to O_RING_1:def 10 :: thesis: ( h is being_an_Amalgam_of_squares & x * y = h /. (len h) )
len h = (len (f ^ g)) + (len <*((f /. (len f)) * (g /. (len g)))*>) by FINSEQ_1:22
.= (len (f ^ g)) + 1 by Lm2 ;
hence ( h is being_an_Amalgam_of_squares & x * y = h /. (len h) ) by A3, A4, Lm3, Lm84; :: thesis: verum