let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for A being non empty Subset of () st A = the carrier of () holds
A is opers_closed

set B = Formal-Series L;
let A be non empty Subset of (); :: thesis: ( A = the carrier of () implies A is opers_closed )
assume A1: A = the carrier of () ; :: thesis: A is opers_closed
A2: for a being Element of L
for v being Element of () st v in A holds
a * v in A
proof
let a be Element of L; :: thesis: for v being Element of () st v in A holds
a * v in A

let v be Element of (); :: thesis: ( v in A implies a * v in A )
assume v in A ; :: thesis: a * v in A
then reconsider p = v as AlgSequence of L by ;
reconsider a9 = a as Element of L ;
a * v = a9 * p by Def2;
hence a * v in A by ; :: thesis: verum
end;
for v, u being Element of () st v in A & u in A holds
v + u in A
proof
let v, u be Element of (); :: thesis: ( v in A & u in A implies v + u in A )
assume ( v in A & u in A ) ; :: thesis: v + u in A
then reconsider p = v, q = u as AlgSequence of L by ;
v + u = p + q by Def2;
hence v + u in A by ; :: thesis: verum
end;
hence A is linearly-closed by ; :: according to POLYALG1:def 4 :: thesis: ( ( for x, y being Element of () st x in A & y in A holds
x * y in A ) & 1. () in A & 0. () in A )

thus for u, v being Element of () st u in A & v in A holds
u * v in A :: thesis: ( 1. () in A & 0. () in A )
proof
let u, v be Element of (); :: thesis: ( u in A & v in A implies u * v in A )
assume ( u in A & v in A ) ; :: thesis: u * v in A
then reconsider p = u, q = v as AlgSequence of L by ;
u * v = p *' q by Def2;
hence u * v in A by ; :: thesis: verum
end;
1. () = 1_. L by Def2
.= 1. () by POLYNOM3:def 10 ;
hence 1. () in A by A1; :: thesis: 0. () in A
0. () = 0_. L by Def2
.= 0. () by POLYNOM3:def 10 ;
hence 0. () in A by A1; :: thesis: verum