let F, G be ext-real-membered set ; :: thesis: for r being real number st r ++ F = r ++ G holds
F = G
let r be real number ; :: thesis: ( r ++ F = r ++ G implies F = G )
assume r ++ F = r ++ G ; :: thesis: F = G
then ( F c= G & G c= F ) by Th135;
hence F = G by XBOOLE_0:def 10; :: thesis: verum