let x, y, z be Element of REAL+ ; :: thesis: x *' (y -' z) = (x *' y) -' (x *' z)

per cases ( z <=' y or x = {} or ( not z <=' y & x <> {} ) ) ;

suppose A1: z <=' y ; :: thesis: x *' (y -' z) = (x *' y) -' (x *' z)

then A2: x *' z <=' x *' y by Th8;
(x *' (y -' z)) + (x *' z) = x *' ((y -' z) + z) by ARYTM_2:13
.= x *' y by A1, Def1
.= ((x *' y) -' (x *' z)) + (x *' z) by A2, Def1 ;
hence x *' (y -' z) = (x *' y) -' (x *' z) by ARYTM_2:11; :: thesis: verum

end;

suppose A3: x = {} ; :: thesis: x *' (y -' z) = (x *' y) -' (x *' z)

then x *' y = {} by ARYTM_2:4;
hence x *' (y -' z) = x *' y by A3, ARYTM_2:4
.= (x *' y) -' (x *' z) by A3, Lm4, ARYTM_2:4 ;
:: thesis: verum

end;

suppose A4: ( not z <=' y & x <> {} ) ; :: thesis: x *' (y -' z) = (x *' y) -' (x *' z)

then A5: not x *' z <=' x *' y by Lm2;
y -' z = {} by A4, Def1;
hence x *' (y -' z) = {} by ARYTM_2:4
.= (x *' y) -' (x *' z) by A5, Def1 ;
:: thesis: verum

end;

end;