let R be non empty right_add-cancelable right-distributive associative commutative left_zeroed doubleLoopStr ; :: thesis: for I being non empty add-closed right-ideal Subset of R
for J, K being Subset of R holds (I % J) % K = I % (J *' K)
let I be non empty add-closed right-ideal Subset of R; :: thesis: for J, K being Subset of R holds (I % J) % K = I % (J *' K)
let J, K be Subset of R; :: thesis: (I % J) % K = I % (J *' K)

A1: now :: thesis: for u being object st u in (I % J) % K holds
u in I % (J *' K)

let u be object ; :: thesis: ( u in (I % J) % K implies u in I % (J *' K) )
assume u in (I % J) % K ; :: thesis: u in I % (J *' K)
then consider a being Element of R such that
A2: u = a and
A3: a * K c= I % J ;

now :: thesis: for v being object st v in a * (J *' K) holds
v in I

let v be object ; :: thesis: ( v in a * (J *' K) implies v in I )
assume v in a * (J *' K) ; :: thesis: v in I
then consider b being Element of R such that
A4: v = a * b and
A5: b in J *' K ;
consider s being FinSequence of the carrier of R such that
A6: Sum s = b and
A7: 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 J & b in K ) by A5;
set q = a * s;
A8: dom (a * s) = dom s by POLYNOM1:def 1;
A9: Seg (len (a * s)) = dom (a * s) by FINSEQ_1:def 3
.= dom s by POLYNOM1:def 1
.= Seg (len s) by FINSEQ_1:def 3 ;
then A10: len (a * s) = len s by FINSEQ_1:6;
for j being Element of NAT st 1 <= j & j <= len (a * s) holds
ex c, d being Element of R st
( (a * s) . j = c * d & c in I % J & d in J )

proof

let j be Element of NAT ; :: thesis: ( 1 <= j & j <= len (a * s) implies ex c, d being Element of R st
( (a * s) . j = c * d & c in I % J & d in J ) )
assume A11: ( 1 <= j & j <= len (a * s) ) ; :: thesis: ex c, d being Element of R st
( (a * s) . j = c * d & c in I % J & d in J )
then consider c, d being Element of R such that
A12: s . j = c * d and
A13: c in J and
A14: d in K by A7, A10;
A15: a * d in { (a * b9) where b9 is Element of R : b9 in K } by A14;
j in Seg (len s) by A9, A11, FINSEQ_1:1;
then A16: j in dom s by FINSEQ_1:def 3;
then A17: s /. j = c * d by A12, PARTFUN1:def 6;
(a * s) . j = (a * s) /. j by A8, A16, PARTFUN1:def 6
.= a * (c * d) by A16, A17, POLYNOM1:def 1
.= (a * d) * c by GROUP_1:def 3 ;
hence ex c, d being Element of R st
( (a * s) . j = c * d & c in I % J & d in J ) by A3, A13, A15; :: thesis: verum

end;

then A18: Sum (a * s) in { (Sum t) where t is FinSequence of the carrier of R : for i being Element of NAT st 1 <= i & i <= len t holds
ex a, b being Element of R st
( t . i = a * b & a in I % J & b in J ) } ;
A19: (I % J) *' J c= I by Th87;
Sum (a * s) = v by A4, A6, BINOM:4;
hence v in I by A18, A19; :: thesis: verum

end;

then a * (J *' K) c= I ;
hence u in I % (J *' K) by A2; :: thesis: verum

end;

now :: thesis: for u being object st u in I % (J *' K) holds
u in (I % J) % K

let u be object ; :: thesis: ( u in I % (J *' K) implies u in (I % J) % K )
assume u in I % (J *' K) ; :: thesis: u in (I % J) % K
then consider a being Element of R such that
A20: u = a and
A21: a * (J *' K) c= I ;

now :: thesis: for v being object st v in a * K holds
v in I % J

let v be object ; :: thesis: ( v in a * K implies v in I % J )
assume v in a * K ; :: thesis: v in I % J
then consider b being Element of R such that
A22: v = a * b and
A23: b in K ;

now :: thesis: for z being object st z in (a * b) * J holds
z in I

let z be object ; :: thesis: ( z in (a * b) * J implies z in I )
assume z in (a * b) * J ; :: thesis: z in I
then consider c being Element of R such that
A24: z = (a * b) * c and
A25: c in J ;
A26: z = a * (c * b) by A24, GROUP_1:def 3;
set q = <*(c * b)*>;
A27: len <*(c * b)*> = 1 by FINSEQ_1:40;
A28: for i being Element of NAT st 1 <= i & i <= len <*(c * b)*> holds
ex x, y being Element of R st
( <*(c * b)*> . i = x * y & x in J & y in K )

proof

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len <*(c * b)*> implies ex x, y being Element of R st
( <*(c * b)*> . i = x * y & x in J & y in K ) )
assume ( 1 <= i & i <= len <*(c * b)*> ) ; :: thesis: ex x, y being Element of R st
( <*(c * b)*> . i = x * y & x in J & y in K )
then <*(c * b)*> . i = <*(c * b)*> . 1 by A27, XXREAL_0:1
.= c * b ;
hence ex x, y being Element of R st
( <*(c * b)*> . i = x * y & x in J & y in K ) by A23, A25; :: thesis: verum

end;

Sum <*(c * b)*> = c * b by BINOM:3;
then c * b in { (Sum t) where t is FinSequence of the carrier of R : for i being Element of NAT st 1 <= i & i <= len t holds
ex a, b being Element of R st
( t . i = a * b & a in J & b in K ) } by A28;
then z in { (a * f) where f is Element of R : f in J *' K } by A26;
hence z in I by A21; :: thesis: verum

end;

then (a * b) * J c= I ;
hence v in I % J by A22; :: thesis: verum

end;

then a * K c= I % J ;
hence u in (I % J) % K by A20; :: thesis: verum

end;

hence (I % J) % K = I % (J *' K) by A1, TARSKI:2; :: thesis: verum