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

v + u in A

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 )

.= 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

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

for v, u being Element of (Formal-Series L) st v in A & u in A holds
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;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

v + u in A

proof

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
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;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

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

1. (Formal-Series L) =
1_. L
by Def2
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;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

.= 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