let F, G be ext-real-membered set ; :: thesis: for f being ext-real number holds (f ** F) \ (f ** G) c= f ** (F \ G)
let f be ext-real number ; :: thesis: (f ** F) \ (f ** G) c= f ** (F \ G)
let i be ext-real number ; :: 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

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