let f, g, h be ext-real number ; :: thesis: {f,g} -- {h} = {(f - h),(g - h)}
thus {f,g} -- {h} = {f,g} ++ {(- h)} by Th15
.= {(f - h),(g - h)} by Th50 ; :: thesis: verum