let R be non empty multLoopStr ; :: thesis: for I, J, K being Subset of R holds (J /\ K) % I = (J % I) /\ (K % I)
let I, J, K be Subset of R; :: thesis: (J /\ K) % I = (J % I) /\ (K % I)

A1: now

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

now

let v be set ; :: thesis: ( v in a * I implies v in J )
assume v in a * I ; :: thesis: v in J
then v in J /\ K by A2;
then consider x being Element of R such that
A3: ( v = x & x in J & x in K ) ;
thus v in J by A3; :: thesis: verum

end;

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

now

let v be set ; :: thesis: ( v in a * I implies v in K )
assume v in a * I ; :: thesis: v in K
then v in J /\ K by A2;
then consider x being Element of R such that
A5: ( v = x & x in J & x in K ) ;
thus v in K by A5; :: thesis: verum

end;

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

end;

now

let u be set ; :: thesis: ( u in (J % I) /\ (K % I) implies u in (J /\ K) % I )
assume u in (J % I) /\ (K % I) ; :: thesis: u in (J /\ K) % I
then consider x being Element of R such that
A6: ( x = u & x in J % I & x in K % I ) ;
consider a being Element of R such that
A7: ( u = a & a * I c= J ) by A6;
consider b being Element of R such that
A8: ( u = b & b * I c= K ) by A6;
for v being set st v in a * I holds
v in J /\ K by A7, A8;
then a * I c= J /\ K by TARSKI:def 3;
hence u in (J /\ K) % I by A7; :: thesis: verum

end;

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