let F, G be ext-real-membered set ; :: thesis: for r being Real holds (F \+\ G) -- r = (F -- r) \+\ (G -- r)
let r be Real; :: thesis: (F \+\ G) -- r = (F -- r) \+\ (G -- r)
thus (F \+\ G) -- r = -- (r -- (F \+\ G)) by Th60
.= -- ((r -- F) \+\ (r -- G)) by Th159
.= (-- (r -- F)) \+\ (-- (r -- G)) by Th8
.= (-- (r -- F)) \+\ (G -- r) by Th60
.= (F -- r) \+\ (G -- r) by Th60 ; :: thesis: verum