let R be non empty right_complementable Abelian add-associative right_zeroed left-distributive left_unital left_zeroed doubleLoopStr ; :: thesis: for I being non empty add-closed left-ideal Subset of R
for J being Subset of R
for K being non empty Subset of R st J c= I holds
I /\ (J + K) = J + (I /\ K)
let I be non empty add-closed left-ideal Subset of R; :: thesis: for J being Subset of R
for K being non empty Subset of R st J c= I holds
I /\ (J + K) = J + (I /\ K)
let J be Subset of R; :: thesis: for K being non empty Subset of R st J c= I holds
I /\ (J + K) = J + (I /\ K)
let K be non empty Subset of R; :: thesis: ( J c= I implies I /\ (J + K) = J + (I /\ K) )
assume A1: J c= I ; :: thesis: I /\ (J + K) = J + (I /\ K)

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

let u be object ; :: thesis: ( u in J + (I /\ K) implies u in I /\ (J + K) )
assume u in J + (I /\ K) ; :: thesis: u in I /\ (J + K)
then consider j, ik being Element of R such that
A3: u = j + ik and
A4: j in J and
A5: ik in I /\ K ;
A6: ex z being Element of R st
( z = ik & z in I & z in K ) by A5;
then reconsider k9 = ik as Element of K ;
u = j + k9 by A3;
then A7: u in J + K by A4;
reconsider j9 = j as Element of I by A1, A4;
reconsider i9 = ik as Element of I by A6;
u = j9 + i9 by A3;
then u in I by Def1;
hence u in I /\ (J + K) by A7; :: thesis: verum

end;

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

let u be object ; :: thesis: ( u in I /\ (J + K) implies u in J + (I /\ K) )
assume u in I /\ (J + K) ; :: thesis: u in J + (I /\ K)
then consider v being Element of R such that
A8: u = v and
A9: v in I and
A10: v in J + K ;
consider j, k being Element of R such that
A11: v = j + k and
A12: j in J and
A13: k in K by A10;
reconsider j9 = j as Element of I by A1, A12;
- j9 in I by Th13;
then (j9 + k) + (- j9) in I by A9, A11, Def1;
then (j9 + (- j9)) + k in I by RLVECT_1:def 3;
then (0. R) + k in I by RLVECT_1:5;
then k in I by ALGSTR_1:def 2;
then k in I /\ K by A13;
hence u in J + (I /\ K) by A8, A11, A12; :: thesis: verum

end;

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