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