the carrier of (Polynom-Ring L) c= the carrier 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

proof

then reconsider A = the carrier of (Polynom-Ring L) as non empty Subset of (Formal-Series L) ;
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;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

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