let F, G be ext-real-membered set ; :: thesis: for f being ExtReal holds (f ** F) \ (f ** G) c= f ** (F \ G)
let f be ExtReal; :: thesis: (f ** F) \ (f ** G) c= f ** (F \ G)
let i be ExtReal; :: according to MEMBERED:def 8 :: thesis: ( not i in (f ** F) \ (f ** G) or i in f ** (F \ G) )
assume A1: i in (f ** F) \ (f ** G) ; :: thesis: i in f ** (F \ G)
then consider w being Element of ExtREAL such that
A2: i = f * w and
A3: w in F by Th188;

now :: thesis: w in F \ G

assume not w in F \ G ; :: thesis: contradiction
then w in G by A3, XBOOLE_0:def 5;
then f * w in f ** G by Th186;
hence contradiction by A1, A2, XBOOLE_0:def 5; :: thesis: verum

end;

hence i in f ** (F \ G) by A2, Th186; :: thesis: verum