set M = LowPositives(Poly) P;
set K = Polynom-Ring R;
X: ( P + P c= P & P * P c= P & SQ R c= P ) by defppc;

let x, y be Element of (Polynom-Ring R); :: thesis:
assume AS: ( x in LowPositives(Poly) P & y in LowPositives(Poly) P ) ; :: thesis:
then consider p being Polynomial of R such that
A: ( x = p & p . (min* { i where i is Nat : p . i <> 0. R } ) in P ) ;
consider q being Polynomial of R such that
B: ( y = q & q . (min* { i where i is Nat : q . i <> 0. R } ) in P ) by AS;
C1: (p . (min* { i where i is Nat : p . i <> 0. R } )) * (q . (min* { i where i is Nat : q . i <> 0. R } )) in P * P by A, B;

then p *' q = 0_. R by POLYNOM3:34;
then (p *' q) . (min* { i where i is Nat : (p *' q) . i <> 0. R } ) = 0. R by FUNCOP_1:7;
then (p *' q) . (min* { i where i is Nat : (p *' q) . i <> 0. R } ) in P by ord3;
then p *' q in { r where r is Polynomial of R : r . (min* { i where i is Nat : r . i <> 0. R } ) in P } ;
hence x * y in LowPositives(Poly) P by A, B, POLYNOM3:def 10; :: thesis:

end;

then p *' q = 0_. R by POLYNOM4:2;
then (p *' q) . (min* { i where i is Nat : (p *' q) . i <> 0. R } ) = 0. R by FUNCOP_1:7;
then (p *' q) . (min* { i where i is Nat : (p *' q) . i <> 0. R } ) in P by ord3;
then p *' q in { r where r is Polynomial of R : r . (min* { i where i is Nat : r . i <> 0. R } ) in P } ;
hence x * y in LowPositives(Poly) P by A, B, POLYNOM3:def 10; :: thesis:

end;

then ( not p is zero & not q is zero ) ;
then (p *' q) . (min* { i where i is Nat : (p *' q) . i <> 0. R } ) in P * P by C1, lemlowp3;
then p *' q in { r where r is Polynomial of R : r . (min* { i where i is Nat : r . i <> 0. R } ) in P } by X;
hence x * y in LowPositives(Poly) P by A, B, POLYNOM3:def 10; :: thesis:

end;

let o be object ; :: thesis:
assume o in SQ (Polynom-Ring R) ; :: thesis:
then consider a being Element of (Polynom-Ring R) such that
X1: ( o = a & a is square ) ;
reconsider p = a as Polynomial of R by POLYNOM3:def 10;
consider b being Element of (Polynom-Ring R) such that
X2: a = b ^2 by X1;
reconsider q = b as Polynomial of R by POLYNOM3:def 10;
X3: p = q *' q by POLYNOM3:def 10, X2;

then p = 0_. R by X3, POLYNOM3:34;
then p . (min* { i where i is Nat : p . i <> 0. R } ) = 0. R by FUNCOP_1:7;
then p . (min* { i where i is Nat : p . i <> 0. R } ) in P by ord3;
hence o in LowPositives(Poly) P by X1; :: thesis:

end;

then reconsider qq = q as non zero Polynomial of R by UPROOTS:def 5;
(q *' q) . (min* { i where i is Nat : (qq *' qq) . i <> 0. R } ) = (q . (min* { i where i is Nat : qq . i <> 0. R } )) * (q . (min* { i where i is Nat : qq . i <> 0. R } )) by lemlowp3;
then (q *' q) . (min* { i where i is Nat : (q *' q) . i <> 0. R } ) = (q . (min* { i where i is Nat : q . i <> 0. R } )) ^2 ;
then (q *' q) . (min* { i where i is Nat : (q *' q) . i <> 0. R } ) is square ;
then (q *' q) . (min* { i where i is Nat : (q *' q) . i <> 0. R } ) in SQ R ;
hence o in LowPositives(Poly) P by X, X1, X3; :: thesis:

end;