the carrier of (Polynom-Ring L) c= the carrier of (Formal-Series L)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (Polynom-Ring L) or x in the carrier of (Formal-Series L) )
assume x in the carrier of (Polynom-Ring L) ; :: thesis: x in the carrier of (Formal-Series L)
then x is AlgSequence of L by POLYNOM3:def 10;
hence x in the carrier of (Formal-Series L) by Def2; :: thesis: verum
end;
then reconsider A = the carrier of (Polynom-Ring L) as non empty Subset of (Formal-Series L) ;
take GenAlg A ; :: thesis: ex A being non empty Subset of (Formal-Series L) st
( A = the carrier of (Polynom-Ring L) & GenAlg A = GenAlg A )
thus ex A being non empty Subset of (Formal-Series L) st
( A = the carrier of (Polynom-Ring L) & GenAlg A = GenAlg A ) ; :: thesis: verum