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

let u be set ; :: 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 & a * (J + K) c= I ) ;

now

let u be set ; :: thesis: ( u in a * K implies u in I )
assume u in a * K ; :: thesis: u in I
then consider j being Element of R such that
A3: ( u = a * j & j in K ) ;
K c= J + K by Th74;
then u in { (a * j') where j' is Element of R : j' in J + K } by A3;
hence u in I by A2; :: thesis: verum

end;

then a * K c= I by TARSKI:def 3;
then A4: u in I % K by A2;

now

let u be set ; :: thesis: ( u in a * J implies u in I )
assume u in a * J ; :: thesis: u in I
then consider j being Element of R such that
A5: ( u = a * j & j in J ) ;
J c= J + K by Th73;
then u in { (a * j') where j' is Element of R : j' in J + K } by A5;
hence u in I by A2; :: thesis: verum

end;

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

end;

now

let u be set ; :: 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 consider x being Element of R such that
A6: ( u = x & x in I % J & x in I % K ) ;
consider a being Element of R such that
A7: ( u = a & a * J c= I ) by A6;
consider b being Element of R such that
A8: ( u = b & b * K c= I ) by A6;

now

let v be set ; :: 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
A9: ( v = a * j & j in J + K ) ;
consider x', y being Element of R such that
A10: ( j = x' + y & x' in J & y in K ) by A9;
A11: v = (a * x') + (b * y) by A7, A8, A9, A10, VECTSP_1:def 11;
A12: a * x' in a * J by A10;
b * y in { (b * j') where j' is Element of R : j' in K } by A10;
hence v in I by A7, A8, A11, A12, Def1; :: thesis: verum

end;

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

end;

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