theorem :: O_RING_1:9

for R being non empty doubleLoopStr
for x, y being Scalar of R st ( ( x is being_an_amalgam_of_squares & ( y is being_a_product_of_squares or y is being_an_amalgam_of_squares ) ) or ( x is being_a_sum_of_amalgams_of_squares & ( y is being_a_square or y is being_a_product_of_squares or y is being_an_amalgam_of_squares ) ) ) holds
x + y is being_a_sum_of_amalgams_of_squares by Lm60, Lm66, Lm67, Lm68, Lm69;