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)} *' 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
A2: Sum s = u and
A3: 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 A4: 1 in dom s by FINSEQ_1:def 3;
A5: 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 A6: 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
A7: s . i = a * b and
A8: a in {(0. R)} and
b in I by A3;
A9: a = 0. R by A8, TARSKI:def 1;
s /. i = a * b by A6, A7, PARTFUN1:def 8;
hence s /. i = 0. R by A9, 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 A4, POLYNOM2:5
.= 0. R by A4, A5 ;
:: thesis: verum

end;

end;

end;

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

end;

now

reconsider o = 0. R as Element of {(0. R)} by TARSKI:def 1;
consider a being Element of I;
let u be set ; :: thesis: ( u in {(0. R)} implies u in {(0. R)} *' I )
assume A10: u in {(0. R)} ; :: thesis: u in {(0. R)} *' I
set q = <*((0. R) * a)*>;
A11: ( len <*((0. R) * a)*> = 1 & <*((0. R) * a)*> . 1 = (0. R) * a ) by FINSEQ_1:57;
A12: 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 A11, 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;

Sum <*((0. R) * a)*> = (0. R) * a by BINOM:3
.= 0. R by BINOM:1
.= u by A10, TARSKI:def 1 ;
hence u in {(0. R)} *' I by A12; :: thesis: verum

end;

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