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 object ; :: 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:57;
( 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 object ; :: 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 r09, t0 being Element of RAT+ such that
A13: t1 = r09 *' t0 and
A14: r09 in A and
A15: t0 in C by A9;
per cases ( r0 <=' r09 or r09 <=' r0 ) ;
suppose r0 <=' r09 ; :: thesis: e in A *' (B + C)
then r0 *' s0 <=' r09 *' s0 by ARYTM_3:82;
then consider s09 being Element of RAT+ such that
A16: r0 *' s0 = r09 *' s09 and
A17: s09 <=' s0 by ARYTM_3:79;
s09 in B by A12, A17, Lm16;
then A18: s09 + t0 in B + C by A15;
e = r09 *' (s09 + t0) by A7, A10, A13, A16, ARYTM_3:57;
hence e in A *' (B + C) by A14, A18; :: thesis: verum
end;
suppose r09 <=' r0 ; :: thesis: e in A *' (B + C)
then r09 *' t0 <=' r0 *' t0 by ARYTM_3:82;
then consider t09 being Element of RAT+ such that
A19: r09 *' t0 = r0 *' t09 and
A20: t09 <=' t0 by ARYTM_3:79;
t09 in C by A15, A20, Lm16;
then A21: s0 + t09 in B + C by A12;
e = r0 *' (s0 + t09) by A7, A10, A13, A19, ARYTM_3:57;
hence e in A *' (B + C) by A11, A21; :: thesis: verum
end;
end;