let f, h, i be ExtReal; :: thesis: {f} -- {h,i} = {(f - h),(f - i)}
thus {f} -- {h,i} = {f} ++ {(- h),(- i)} by Th10
.= {(f - h),(f - i)} by Th44 ; :: thesis: verum