let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for A being non empty Subset of (Formal-Series L) st A = the carrier of (Polynom-Ring L) holds
A is opers_closed
let A be non empty Subset of (Formal-Series L); :: thesis: ( A = the carrier of (Polynom-Ring L) implies A is opers_closed )
assume A1: A = the carrier of (Polynom-Ring L) ; :: thesis: A is opers_closed
set B = Formal-Series L;
thus A is linearly-closed :: according to POLYALG1:def 4 :: thesis: ( ( for x, y being Element of (Formal-Series L) st x in A & y in A holds
x * y in A ) & 1. (Formal-Series L) in A & 0. (Formal-Series L) in A )

proof

thus for v, u being Element of (Formal-Series L) st v in A & u in A holds
v + u in A :: according to VECTSP_4:def 1 :: thesis: for b₁ being Element of the carrier of L
for b₂ being Element of the carrier of (Formal-Series L) holds
( not b₂ in A or b₁ * b₂ in A )

proof

let v, u be Element of (Formal-Series L); :: thesis: ( v in A & u in A implies v + u in A )
assume A2: ( v in A & u in A ) ; :: thesis: v + u in A
reconsider p = v, q = u as AlgSequence of L by A1, A2, POLYNOM3:def 12;
v + u = p + q by Def2;
hence v + u in A by A1, POLYNOM3:def 12; :: thesis: verum

end;

thus for a being Element of L
for v being Element of (Formal-Series L) st v in A holds
a * v in A :: thesis: verum

proof

let a be Element of L; :: thesis: for v being Element of (Formal-Series L) st v in A holds
a * v in A
let v be Element of (Formal-Series L); :: thesis: ( v in A implies a * v in A )
assume A3: v in A ; :: thesis: a * v in A
reconsider a' = a as Element of L ;
reconsider p = v as AlgSequence of L by A1, A3, POLYNOM3:def 12;
a * v = a' * p by Def2;
hence a * v in A by A1, POLYNOM3:def 12; :: thesis: verum

end;

end;

thus for u, v being Element of (Formal-Series L) st u in A & v in A holds
u * v in A :: thesis: ( 1. (Formal-Series L) in A & 0. (Formal-Series L) in A )

proof

let u, v be Element of (Formal-Series L); :: thesis: ( u in A & v in A implies u * v in A )
assume A4: ( u in A & v in A ) ; :: thesis: u * v in A
reconsider p = u, q = v as AlgSequence of L by A1, A4, POLYNOM3:def 12;
u * v = p *' q by Def2;
hence u * v in A by A1, POLYNOM3:def 12; :: thesis: verum

end;

1. (Formal-Series L) = 1_. L by Def2
.= 1. (Polynom-Ring L) by POLYNOM3:def 12 ;
hence 1. (Formal-Series L) in A by A1; :: thesis: 0. (Formal-Series L) in A
0. (Formal-Series L) = 0_. L by Def2
.= 0. (Polynom-Ring L) by POLYNOM3:def 12 ;
hence 0. (Formal-Series L) in A by A1; :: thesis: verum