let F, G be ext-real-membered set ; :: thesis: for r being Real st r <> 0 holds
r ** (F \ G) = (r ** F) \ (r ** G)
let r be Real; :: thesis: ( r <> 0 implies r ** (F \ G) = (r ** F) \ (r ** G) )
assume A1: r <> 0 ; :: thesis: r ** (F \ G) = (r ** F) \ (r ** G)
A2: r ** (F \ G) c= (r ** F) \ (r ** G)

proof

let i be ExtReal; :: according to MEMBERED:def 8 :: thesis: ( not i in r ** (F \ G) or i in (r ** F) \ (r ** G) )
assume i in r ** (F \ G) ; :: thesis: i in (r ** F) \ (r ** G)
then consider w being Element of ExtREAL such that
A3: i = r * w and
A4: w in F \ G by Th188;

A5: now :: thesis: not r * w in r ** G

assume r * w in r ** G ; :: thesis: contradiction
then consider w1 being Element of ExtREAL such that
A6: r * w = r * w1 and
A7: w1 in G by Th188;
w = w1 by A1, A6, XXREAL_3:68;
hence contradiction by A4, A7, XBOOLE_0:def 5; :: thesis: verum

end;

r * w in r ** F by A4, Th186;
hence i in (r ** F) \ (r ** G) by A3, A5, XBOOLE_0:def 5; :: thesis: verum

end;

(r ** F) \ (r ** G) c= r ** (F \ G) by Th190;
hence r ** (F \ G) = (r ** F) \ (r ** G) by A2; :: thesis: verum