let z, y, x 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