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