let F be ext-real-membered set ; :: thesis: for f being ExtReal
for e being set st e in f ++ F holds
ex w being Element of ExtREAL st
( e = f + w & w in F )
let f be ExtReal; :: thesis: for e being set st e in f ++ F holds
ex w being Element of ExtREAL st
( e = f + w & w in F )
let e be set ; :: thesis: ( e in f ++ F implies ex w being Element of ExtREAL st
( e = f + w & w in F ) )
f ++ F = { (f + w) where w is Element of ExtREAL : w in F } by Th133;
hence ( e in f ++ F implies ex w being Element of ExtREAL st
( e = f + w & w in F ) ) ; :: thesis: verum