let R be non empty left_unital left_zeroed doubleLoopStr ; :: thesis: for I, J being non empty Subset of R st I,J are_co-prime holds
I /\ J c= (I + J) *' (I /\ J)
let I, J be non empty Subset of R; :: thesis: ( I,J are_co-prime implies I /\ J c= (I + J) *' (I /\ J) )
assume I,J are_co-prime ; :: thesis: I /\ J c= (I + J) *' (I /\ J)
then A1: I + J = the carrier of R ;
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in I /\ J or u in (I + J) *' (I /\ J) )
assume A2: u in I /\ J ; :: thesis: u in (I + J) *' (I /\ J)
then reconsider u9 = u as Element of R ;
set q = <*((1. R) * u9)*>;
A3: len <*((1. R) * u9)*> = 1 by FINSEQ_1:39;
A4: for i being Element of NAT st 1 <= i & i <= len <*((1. R) * u9)*> holds
ex x, y being Element of R st
( <*((1. R) * u9)*> . i = x * y & x in I + J & y in I /\ J )
proof
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len <*((1. R) * u9)*> implies ex x, y being Element of R st
( <*((1. R) * u9)*> . i = x * y & x in I + J & y in I /\ J ) )
assume A5: ( 1 <= i & i <= len <*((1. R) * u9)*> ) ; :: thesis: ex x, y being Element of R st
( <*((1. R) * u9)*> . i = x * y & x in I + J & y in I /\ J )
take 1. R ; :: thesis: ex y being Element of R st
( <*((1. R) * u9)*> . i = (1. R) * y & 1. R in I + J & y in I /\ J )
take u9 ; :: thesis: ( <*((1. R) * u9)*> . i = (1. R) * u9 & 1. R in I + J & u9 in I /\ J )
i = 1 by A3, A5, XXREAL_0:1;
hence ( <*((1. R) * u9)*> . i = (1. R) * u9 & 1. R in I + J & u9 in I /\ J ) by A1, A2, FINSEQ_1:40; :: thesis: verum
end;
Sum <*((1. R) * u9)*> = (1. R) * u9 by BINOM:3
.= u9 ;
hence u in (I + J) *' (I /\ J) by A4; :: thesis: verum