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
set B = Formal-Series L;
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
A2: for a being Element of L
for v being Element of (Formal-Series L) st v in A holds
a * v in A
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 v in A ; :: thesis: a * v in A
then reconsider p = v as AlgSequence of L by A1, POLYNOM3:def 10;
reconsider a9 = a as Element of L ;
a * v = a9 * p by Def2;
hence a * v in A by A1, POLYNOM3:def 10; :: thesis: verum
end;
for v, u being Element of (Formal-Series L) st v in A & u in A holds
v + u 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 ( v in A & u in A ) ; :: thesis: v + u in A
then reconsider p = v, q = u as AlgSequence of L by A1, POLYNOM3:def 10;
v + u = p + q by Def2;
hence v + u in A by A1, POLYNOM3:def 10; :: thesis: verum
end;
hence A is linearly-closed by A2, VECTSP_4:def 1; :: 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 )
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 ( u in A & v in A ) ; :: thesis: u * v in A
then reconsider p = u, q = v as AlgSequence of L by A1, POLYNOM3:def 10;
u * v = p *' q by Def2;
hence u * v in A by A1, POLYNOM3:def 10; :: thesis: verum
end;
1. (Formal-Series L) = 1_. L by Def2
.= 1. (Polynom-Ring L) by POLYNOM3:def 10 ;
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 10 ;
hence 0. (Formal-Series L) in A by A1; :: thesis: verum