theorem :: O_RING_1:38

for R being non empty doubleLoopStr
for x, y being Scalar of R st ( ( x is generated_from_squares & y is being_a_square ) or ( x is generated_from_squares & y is being_a_sum_of_squares ) or ( x is generated_from_squares & y is being_a_product_of_squares ) or ( x is generated_from_squares & y is being_a_sum_of_products_of_squares ) or ( x is generated_from_squares & y is being_an_amalgam_of_squares ) or ( x is generated_from_squares & y is being_a_sum_of_amalgams_of_squares ) or ( x is generated_from_squares & y is generated_from_squares ) ) holds
x + y is generated_from_squares by Lm36, Lm43, Lm64, Lm76, Lm77, Lm78, Lm79;