let x, y, z be Element of REAL+ ; :: thesis: ( not z <=' y & x <> {} implies [{},(x *' (z -' y))] = (x *' y) - (x *' z) )
assume ( not z <=' y & x <> {} ) ; :: thesis: [{},(x *' (z -' y))] = (x *' y) - (x *' z)
then A1: not x *' z <=' x *' y by Lm2;
thus [{},(x *' (z -' y))] = [{},((x *' z) -' (x *' y))] by Lm14
.= (x *' y) - (x *' z) by A1, Def2 ; :: thesis: verum