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

now

let u be set ; :: thesis: ( u in I /\ J implies u in (I + J) *' (I /\ J) )
assume A2: u in I /\ J ; :: thesis: u in (I + J) *' (I /\ J)
then consider g being Element of R such that
A3: ( u = g & g in I & g in J ) ;
reconsider u' = u as Element of R by A3;
set q = <*((1. R) * u')*>;
A4: len <*((1. R) * u')*> = 1 by FINSEQ_1:56;
A5: for i being Element of NAT st 1 <= i & i <= len <*((1. R) * u')*> holds
ex x, y being Element of R st
( <*((1. R) * u')*> . 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) * u')*> implies ex x, y being Element of R st
( <*((1. R) * u')*> . i = x * y & x in I + J & y in I /\ J ) )
assume ( 1 <= i & i <= len <*((1. R) * u')*> ) ; :: thesis: ex x, y being Element of R st
( <*((1. R) * u')*> . i = x * y & x in I + J & y in I /\ J )
then A6: i = 1 by A4, XXREAL_0:1;
take 1. R ; :: thesis: ex y being Element of R st
( <*((1. R) * u')*> . i = (1. R) * y & 1. R in I + J & y in I /\ J )
take u' ; :: thesis: ( <*((1. R) * u')*> . i = (1. R) * u' & 1. R in I + J & u' in I /\ J )
thus ( <*((1. R) * u')*> . i = (1. R) * u' & 1. R in I + J & u' in I /\ J ) by A1, A2, A6, FINSEQ_1:57; :: thesis: verum

end;

Sum <*((1. R) * u')*> = (1. R) * u' by BINOM:3
.= u' by VECTSP_1:def 19 ;
hence u in (I + J) *' (I /\ J) by A5; :: thesis: verum

end;

hence I /\ J c= (I + J) *' (I /\ J) by TARSKI:def 3; :: thesis: verum