let A, B, C be Element of DEDEKIND_CUTS ; :: thesis: A *' (B + C) = (A *' B) + (A *' C)
thus A *' (B + C) c= (A *' B) + (A *' C) :: according to XBOOLE_0:def 10 :: thesis: (A *' B) + (A *' C) c= A *' (B + C)

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in A *' (B + C) or e in (A *' B) + (A *' C) )
assume e in A *' (B + C) ; :: thesis: e in (A *' B) + (A *' C)
then consider r0, v0 being Element of RAT+ such that
A1: e = r0 *' v0 and
A2: r0 in A and
A3: v0 in B + C ;
consider s0, t0 being Element of RAT+ such that
A4: v0 = s0 + t0 and
A5: s0 in B and
A6: t0 in C by A3;
A7: r0 *' s0 in A *' B by A2, A5;
A8: r0 *' t0 in A *' C by A2, A6;
e = (r0 *' s0) + (r0 *' t0) by A1, A4, ARYTM_3:63;
hence e in (A *' B) + (A *' C) by A7, A8; :: thesis: verum

end;

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in (A *' B) + (A *' C) or e in A *' (B + C) )
assume e in (A *' B) + (A *' C) ; :: thesis: e in A *' (B + C)
then consider s1, t1 being Element of RAT+ such that
A9: e = s1 + t1 and
A10: s1 in A *' B and
A11: t1 in A *' C ;
consider r0, s0 being Element of RAT+ such that
A12: s1 = r0 *' s0 and
A13: r0 in A and
A14: s0 in B by A10;
consider r0', t0 being Element of RAT+ such that
A15: t1 = r0' *' t0 and
A16: r0' in A and
A17: t0 in C by A11;

per cases ( r0 <=' r0' or r0' <=' r0 ) ;

suppose r0 <=' r0' ; :: thesis: e in A *' (B + C)

then r0 *' s0 <=' r0' *' s0 by ARYTM_3:90;
then consider s0' being Element of RAT+ such that
A18: r0 *' s0 = r0' *' s0' and
A19: s0' <=' s0 by ARYTM_3:87;
s0' in B by A14, A19, Lm16;
then A20: s0' + t0 in B + C by A17;
e = r0' *' (s0' + t0) by A9, A12, A15, A18, ARYTM_3:63;
hence e in A *' (B + C) by A16, A20; :: thesis: verum

end;

suppose r0' <=' r0 ; :: thesis: e in A *' (B + C)

then r0' *' t0 <=' r0 *' t0 by ARYTM_3:90;
then consider t0' being Element of RAT+ such that
A21: r0' *' t0 = r0 *' t0' and
A22: t0' <=' t0 by ARYTM_3:87;
t0' in C by A17, A22, Lm16;
then A23: s0 + t0' in B + C by A14;
e = r0 *' (s0 + t0') by A9, A12, A15, A21, ARYTM_3:63;
hence e in A *' (B + C) by A13, A23; :: thesis: verum

end;

end;