let R be non empty right_add-cancelable right_zeroed right-distributive left_zeroed doubleLoopStr ; :: thesis: for I being add-closed Subset of R
for J, K being non empty right-ideal Subset of R holds I % (J + K) = (I % J) /\ (I % K)
let I be add-closed Subset of R; :: thesis: for J, K being non empty right-ideal Subset of R holds I % (J + K) = (I % J) /\ (I % K)
let J, K be non empty right-ideal Subset of R; :: thesis: I % (J + K) = (I % J) /\ (I % K)

A1: now :: thesis: for u being object st u in I % (J + K) holds
u in (I % J) /\ (I % K)

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

now :: thesis: for u being object st u in a * J holds
u in I

let u be object ; :: thesis: ( u in a * J implies u in I )
assume u in a * J ; :: thesis: u in I
then A4: ex j being Element of R st
( u = a * j & j in J ) ;
J c= J + K by Th73;
then u in { (a * j9) where j9 is Element of R : j9 in J + K } by A4;
hence u in I by A3; :: thesis: verum

end;

then a * J c= I ;
then A5: u in I % J by A2;

now :: thesis: for u being object st u in a * K holds
u in I

let u be object ; :: thesis: ( u in a * K implies u in I )
assume u in a * K ; :: thesis: u in I
then A6: ex j being Element of R st
( u = a * j & j in K ) ;
K c= J + K by Th74;
then u in { (a * j9) where j9 is Element of R : j9 in J + K } by A6;
hence u in I by A3; :: thesis: verum

end;

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

end;

now :: thesis: for u being object st u in (I % J) /\ (I % K) holds
u in I % (J + K)

let u be object ; :: thesis: ( u in (I % J) /\ (I % K) implies u in I % (J + K) )
assume u in (I % J) /\ (I % K) ; :: thesis: u in I % (J + K)
then A7: ex x being Element of R st
( u = x & x in I % J & x in I % K ) ;
then consider a being Element of R such that
A8: u = a and
A9: a * J c= I ;
consider b being Element of R such that
A10: u = b and
A11: b * K c= I by A7;

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 j being Element of R such that
A12: v = a * j and
A13: j in J + K ;
consider x9, y being Element of R such that
A14: j = x9 + y and
A15: ( x9 in J & y in K ) by A13;
A16: ( a * x9 in a * J & b * y in { (b * j9) where j9 is Element of R : j9 in K } ) by A15;
v = (a * x9) + (b * y) by A8, A10, A12, A14, VECTSP_1:def 2;
hence v in I by A9, A11, A16, Def1; :: thesis: verum

end;

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

end;

hence I % (J + K) = (I % J) /\ (I % K) by A1, TARSKI:2; :: thesis: verum