set M = { (S-Poly (p1,p2,T)) where p1, p2 is Polynomial of n,L : ( p1 in P & p2 in P ) } ;

now :: thesis: 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))

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; :: thesis: verumu in the carrier of (Polynom-Ring (n,L))

let u be object ; :: thesis: ( 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 ) } ; :: thesis: 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; :: thesis: verum

end;assume u in { (S-Poly (p1,p2,T)) where p1, p2 is Polynomial of n,L : ( p1 in P & p2 in P ) } ; :: thesis: 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; :: thesis: verum