let R be non empty left_add-cancelable right_zeroed left-distributive left_zeroed doubleLoopStr ; :: thesis: for I being non empty Subset of R holds {(0. R)} *' I = {(0. R)}
let I be non empty Subset of R; :: thesis: {(0. R)} *' I = {(0. R)}

A1: now

let u be set ; :: thesis: ( u in {(0. R)} implies u in {(0. R)} *' I )
assume A2: u in {(0. R)} ; :: thesis: u in {(0. R)} *' I
consider a being Element of I;
set q = <*((0. R) * a)*>;
A3: Sum <*((0. R) * a)*> = (0. R) * a by BINOM:3
.= 0. R by BINOM:1
.= u by A2, TARSKI:def 1 ;
A4: ( len <*((0. R) * a)*> = 1 & <*((0. R) * a)*> . 1 = (0. R) * a ) by FINSEQ_1:57;
reconsider o = 0. R as Element of {(0. R)} by TARSKI:def 1;
for i being Element of NAT st 1 <= i & i <= len <*((0. R) * a)*> holds
ex b, r being Element of R st
( <*((0. R) * a)*> . i = b * r & b in {(0. R)} & r in I )

proof

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len <*((0. R) * a)*> implies ex b, r being Element of R st
( <*((0. R) * a)*> . i = b * r & b in {(0. R)} & r in I ) )
assume ( 1 <= i & i <= len <*((0. R) * a)*> ) ; :: thesis: ex b, r being Element of R st
( <*((0. R) * a)*> . i = b * r & b in {(0. R)} & r in I )
then <*((0. R) * a)*> . i = o * a by A4, XXREAL_0:1;
hence ex b, r being Element of R st
( <*((0. R) * a)*> . i = b * r & b in {(0. R)} & r in I ) ; :: thesis: verum

end;

hence u in {(0. R)} *' I by A3; :: thesis: verum

end;

now

let u be set ; :: thesis: ( u in {(0. R)} *' I implies u in {(0. R)} )
assume u in {(0. R)} *' I ; :: thesis: u in {(0. R)}
then consider s being FinSequence of the carrier of R such that
A5: ( Sum s = u & ( for i being Element of NAT st 1 <= i & i <= len s holds
ex a, b being Element of R st
( s . i = a * b & a in {(0. R)} & b in I ) ) ) ;

now

per cases ( len s = 0 or len s <> 0 ) ;

case len s = 0 ; :: thesis: Sum s = 0. R

then s = <*> the carrier of R ;
hence Sum s = 0. R by RLVECT_1:60; :: thesis: verum

end;

case len s <> 0 ; :: thesis: Sum s = 0. R

then 1 <= len s by NAT_1:14;
then 1 in Seg (len s) by FINSEQ_1:3;
then A6: 1 in dom s by FINSEQ_1:def 3;
A7: for i being Element of NAT st i in dom s holds
s /. i = 0. R

proof

let i be Element of NAT ; :: thesis: ( i in dom s implies s /. i = 0. R )
assume A8: i in dom s ; :: thesis: s /. i = 0. R
then i in Seg (len s) by FINSEQ_1:def 3;
then ( 1 <= i & i <= len s ) by FINSEQ_1:3;
then consider a, b being Element of R such that
A9: ( s . i = a * b & a in {(0. R)} & b in I ) by A5;
A10: s /. i = a * b by A8, A9, PARTFUN1:def 8;
a = 0. R by A9, TARSKI:def 1;
hence s /. i = 0. R by A10, BINOM:1; :: thesis: verum

end;

then for i being Element of NAT st i in dom s & i <> 1 holds
s /. i = 0. R ;
hence Sum s = s /. 1 by A6, POLYNOM2:5
.= 0. R by A6, A7 ;
:: thesis: verum

end;

end;

end;

hence u in {(0. R)} by A5, TARSKI:def 1; :: thesis: verum

end;

hence {(0. R)} *' I = {(0. R)} by A1, TARSKI:2; :: thesis: verum