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 :: thesis: for u being object st u in {(0. R)} *' I holds
u in {(0. R)}
let u be object ; :: 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 :: thesis: ( ( len s = 0 & Sum s = 0. R ) or ( len s <> 0 & Sum s = 0. R ) )
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:43; :: 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:1;
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:1;
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 6;
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:3
.= 0. R by A4, A5 ;
:: thesis: verum
end;
end;
end;
hence u in {(0. R)} by A2, TARSKI:def 1; :: thesis: verum
end;
now :: thesis: for u being object st u in {(0. R)} holds
u in {(0. R)} *' I
reconsider o = 0. R as Element of {(0. R)} by TARSKI:def 1;
set a = the Element of I;
let u be object ; :: 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) * the Element of I)*>;
A11: ( len <*((0. R) * the Element of I)*> = 1 & <*((0. R) * the Element of I)*> . 1 = (0. R) * the Element of I ) by FINSEQ_1:40;
A12: for i being Element of NAT st 1 <= i & i <= len <*((0. R) * the Element of I)*> holds
ex b, r being Element of R st
( <*((0. R) * the Element of I)*> . i = b * r & b in {(0. R)} & r in I )
proof
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len <*((0. R) * the Element of I)*> implies ex b, r being Element of R st
( <*((0. R) * the Element of I)*> . i = b * r & b in {(0. R)} & r in I ) )
assume ( 1 <= i & i <= len <*((0. R) * the Element of I)*> ) ; :: thesis: ex b, r being Element of R st
( <*((0. R) * the Element of I)*> . i = b * r & b in {(0. R)} & r in I )
then <*((0. R) * the Element of I)*> . i = o * the Element of I by A11, XXREAL_0:1;
hence ex b, r being Element of R st
( <*((0. R) * the Element of I)*> . i = b * r & b in {(0. R)} & r in I ) ; :: thesis: verum
end;
Sum <*((0. R) * the Element of I)*> = (0. R) * the Element of I 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