let R be non empty add-cancelable right_zeroed associative well-unital distributive left_zeroed doubleLoopStr ; :: thesis: for I being non empty add-closed right-ideal Subset of R
for J being non empty add-closed left-ideal Subset of R holds sqrt (I *' J) = sqrt (I /\ J)
let I be non empty add-closed right-ideal Subset of R; :: thesis: for J being non empty add-closed left-ideal Subset of R holds sqrt (I *' J) = sqrt (I /\ J)
let J be non empty add-closed left-ideal Subset of R; :: thesis: sqrt (I *' J) = sqrt (I /\ J)

A1: now

let u be set ; :: thesis: ( u in sqrt (I *' J) implies u in sqrt (I /\ J) )
assume u in sqrt (I *' J) ; :: thesis: u in sqrt (I /\ J)
then consider d being Element of R such that
A2: ( u = d & ex m being Element of NAT st d |^ m in I *' J ) ;
consider m being Element of NAT such that
A3: d |^ m in I *' J by A2;
consider s being FinSequence of the carrier of R such that
A4: ( d |^ m = Sum s & ( 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 I & b in J ) ) ) by A3;
consider f being Function of NAT ,the carrier of R such that
A5: ( Sum s = f . (len s) & f . 0 = 0. R & ( for j being Element of NAT
for v being Element of R st j < len s & v = s . (j + 1) holds
f . (j + 1) = (f . j) + v ) ) by RLVECT_1:def 13;
defpred S₁[ Element of NAT ] means f . $1 in I /\ J;
( f . 0 in I & f . 0 in J ) by A5, Th2, Th3;
then A6: S₁[ 0 ] ;

A7: now

let j be Element of NAT ; :: thesis: ( 0 <= j & j < len s & S₁[j] implies S₁[j + 1] )
assume A8: ( 0 <= j & j < len s ) ; :: thesis: ( S₁[j] implies S₁[j + 1] )
thus ( S₁[j] implies S₁[j + 1] ) :: thesis: verum

proof

assume f . j in I /\ J ; :: thesis: S₁[j + 1]
then consider g being Element of R such that
A9: ( g = f . j & g in I & g in J ) ;
A10: j + 1 <= len s by A8, NAT_1:13;
A11: 0 + 1 <= j + 1 by XREAL_1:8;
then j + 1 in Seg (len s) by A10, FINSEQ_1:3;
then j + 1 in dom s by FINSEQ_1:def 3;
then A12: s . (j + 1) = s /. (j + 1) by PARTFUN1:def 8;
then A13: f . (j + 1) = (f . j) + (s /. (j + 1)) by A5, A8;
consider a, b being Element of R such that
A14: ( s . (j + 1) = a * b & a in I & b in J ) by A4, A10, A11;
( s /. (j + 1) in I & s /. (j + 1) in J ) by A12, A14, Def2, Def3;
then ( f . (j + 1) in I & f . (j + 1) in J ) by A9, A13, Def1;
hence S₁[j + 1] ; :: thesis: verum

end;

end;

for j being Element of NAT st 0 <= j & j <= len s holds
S₁[j] from POLYNOM2:sch 4(A6, A7);
then Sum s in I /\ J by A5;
hence u in sqrt (I /\ J) by A2, A4; :: thesis: verum

end;

now

let u be set ; :: thesis: ( u in sqrt (I /\ J) implies u in sqrt (I *' J) )
assume u in sqrt (I /\ J) ; :: thesis: u in sqrt (I *' J)
then consider d being Element of R such that
A15: ( u = d & ex m being Element of NAT st d |^ m in I /\ J ) ;
consider m being Element of NAT such that
A16: d |^ m in I /\ J by A15;
consider g being Element of R such that
A17: ( d |^ m = g & g in I & g in J ) by A16;
set q = <*((d |^ m) * (d |^ m))*>;
A18: len <*((d |^ m) * (d |^ m))*> = 1 by FINSEQ_1:57;
A19: for i being Element of NAT st 1 <= i & i <= len <*((d |^ m) * (d |^ m))*> holds
ex x, y being Element of R st
( <*((d |^ m) * (d |^ m))*> . i = x * y & x in I & y in J )

proof

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len <*((d |^ m) * (d |^ m))*> implies ex x, y being Element of R st
( <*((d |^ m) * (d |^ m))*> . i = x * y & x in I & y in J ) )
assume A20: ( 1 <= i & i <= len <*((d |^ m) * (d |^ m))*> ) ; :: thesis: ex x, y being Element of R st
( <*((d |^ m) * (d |^ m))*> . i = x * y & x in I & y in J )
then i in Seg (len <*((d |^ m) * (d |^ m))*>) by FINSEQ_1:3;
then i in dom <*((d |^ m) * (d |^ m))*> by FINSEQ_1:def 3;
then A21: <*((d |^ m) * (d |^ m))*> . i = <*((d |^ m) * (d |^ m))*> /. i by PARTFUN1:def 8;
then <*((d |^ m) * (d |^ m))*> /. i = <*((d |^ m) * (d |^ m))*> . 1 by A18, A20, XXREAL_0:1
.= (d |^ m) * (d |^ m) by FINSEQ_1:57 ;
hence ex x, y being Element of R st
( <*((d |^ m) * (d |^ m))*> . i = x * y & x in I & y in J ) by A17, A21; :: thesis: verum

end;

d |^ (m + m) = (d |^ m) * (d |^ m) by BINOM:11
.= Sum <*((d |^ m) * (d |^ m))*> by BINOM:3 ;
then d |^ (m + m) in I *' J by A19;
hence u in sqrt (I *' J) by A15; :: thesis: verum

end;

hence sqrt (I *' J) = sqrt (I /\ J) by A1, TARSKI:2; :: thesis: verum