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) /\ (r ** G) c= r ** (F /\ G)
proof
let j be ExtReal; :: according to MEMBERED:def 8 :: thesis: ( not j in (r ** F) /\ (r ** G) or j in r ** (F /\ G) )
assume A3: j in (r ** F) /\ (r ** G) ; :: thesis: j in r ** (F /\ G)
then j in r ** F by XBOOLE_0:def 4;
then consider w being Element of ExtREAL such that
A4: j = r * w and
A5: w in F by Th188;
j in r ** G by A3, XBOOLE_0:def 4;
then consider w1 being Element of ExtREAL such that
A6: j = r * w1 and
A7: w1 in G by Th188;
w = w1 by A1, A4, A6, XXREAL_3:68;
then w in F /\ G by A5, A7, XBOOLE_0:def 4;
hence j in r ** (F /\ G) by A4, Th186; :: thesis: verum
end;
r ** (F /\ G) c= (r ** F) /\ (r ** G) by Th83;
hence r ** (F /\ G) = (r ** F) /\ (r ** G) by A2; :: thesis: verum