let F, G be ext-real-membered set ; :: thesis: for r being real number holds (F \+\ G) -- r = (F -- r) \+\ (G -- r)
let r be real number ; :: thesis: (F \+\ G) -- r = (F -- r) \+\ (G -- r)
thus (F \+\ G) -- r = -- (r -- (F \+\ G)) by Th66
.= -- ((r -- F) \+\ (r -- G)) by Th165
.= (-- (r -- F)) \+\ (-- (r -- G)) by Th14
.= (-- (r -- F)) \+\ (G -- r) by Th66
.= (F -- r) \+\ (G -- r) by Th66 ; :: thesis: verum