set M = { (S-Poly (p1,p2,T)) where p1, p2 is Polynomial of n,L : ( p1 in P & p2 in P ) } ;
now for u being object st u in { (S-Poly (p1,p2,T)) where p1, p2 is Polynomial of n,L : ( p1 in P & p2 in P ) } holds
u in the carrier of (Polynom-Ring (n,L))let u be
object ;
( u in { (S-Poly (p1,p2,T)) where p1, p2 is Polynomial of n,L : ( p1 in P & p2 in P ) } implies u in the carrier of (Polynom-Ring (n,L)) )assume
u in { (S-Poly (p1,p2,T)) where p1, p2 is Polynomial of n,L : ( p1 in P & p2 in P ) }
;
u in the carrier of (Polynom-Ring (n,L))then
ex
p1,
p2 being
Polynomial of
n,
L st
(
u = S-Poly (
p1,
p2,
T) &
p1 in P &
p2 in P )
;
hence
u in the
carrier of
(Polynom-Ring (n,L))
by POLYNOM1:def 11;
verum end;
hence
{ (S-Poly (p1,p2,T)) where p1, p2 is Polynomial of n,L : ( p1 in P & p2 in P ) } is Subset of (Polynom-Ring (n,L))
by TARSKI:def 3; verum