let F, G, H be ext-real-membered set ; :: thesis: (F ** G) ** H = F ** (G ** H)
let i be ExtReal; :: according to MEMBERED:def 14 :: thesis: ( ( not i in (F ** G) ** H or i in F ** (G ** H) ) & ( not i in F ** (G ** H) or i in (F ** G) ** H ) )
hereby :: thesis: ( not i in F ** (G ** H) or i in (F ** G) ** H )
assume i in (F ** G) ** H ; :: thesis: i in F ** (G ** H)
then consider w, w1 being Element of ExtREAL such that
A1: i = w * w1 and
A2: w in F ** G and
A3: w1 in H ;
consider w2, w3 being Element of ExtREAL such that
A4: w = w2 * w3 and
A5: w2 in F and
A6: w3 in G by A2;
( i = w2 * (w3 * w1) & w3 * w1 in G ** H ) by A1, A3, A4, A6, XXREAL_3:66;
hence i in F ** (G ** H) by A5; :: thesis: verum
end;
assume i in F ** (G ** H) ; :: thesis: i in (F ** G) ** H
then consider w, w1 being Element of ExtREAL such that
A7: ( i = w * w1 & w in F ) and
A8: w1 in G ** H ;
consider w2, w3 being Element of ExtREAL such that
A9: ( w1 = w2 * w3 & w2 in G ) and
A10: w3 in H by A8;
( i = (w * w2) * w3 & w * w2 in F ** G ) by A7, A9, XXREAL_3:66;
hence i in (F ** G) ** H by A10; :: thesis: verum