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 & t0 in C ) by A3;
A6: e = (r0 *' s0) + (r0 *' t0) by A1, A4, ARYTM_3:63;
( r0 *' s0 in A *' B & r0 *' t0 in A *' C ) by A2, A5;
hence e in (A *' B) + (A *' C) by A6; :: 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
A7: e = s1 + t1 and
A8: s1 in A *' B and
A9: t1 in A *' C ;
consider r0, s0 being Element of RAT+ such that
A10: s1 = r0 *' s0 and
A11: r0 in A and
A12: s0 in B by A8;
consider r0', t0 being Element of RAT+ such that
A13: t1 = r0' *' t0 and
A14: r0' in A and
A15: t0 in C by A9;

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
A16: r0 *' s0 = r0' *' s0' and
A17: s0' <=' s0 by ARYTM_3:87;
s0' in B by A12, A17, Lm16;
then A18: s0' + t0 in B + C by A15;
e = r0' *' (s0' + t0) by A7, A10, A13, A16, ARYTM_3:63;
hence e in A *' (B + C) by A14, A18; :: 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
A19: r0' *' t0 = r0 *' t0' and
A20: t0' <=' t0 by ARYTM_3:87;
t0' in C by A15, A20, Lm16;
then A21: s0 + t0' in B + C by A12;
e = r0 *' (s0 + t0') by A7, A10, A13, A19, ARYTM_3:63;
hence e in A *' (B + C) by A11, A21; :: thesis: verum

end;

end;