let F, G, H be ext-real-membered set ; :: thesis: (F ** G) ** H = F ** (G ** H)
let i be ext-real number ; :: 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;
A7: i = w2 * (w3 * w1) by A1, A4, XXREAL_3:77;
w3 * w1 in G ** H by A6, A3;
hence i in F ** (G ** H) by A5, A7; :: 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
A8: i = w * w1 and
A9: w in F and
A10: w1 in G ** H ;
consider w2, w3 being Element of ExtREAL such that
A11: w1 = w2 * w3 and
A12: w2 in G and
A13: w3 in H by A10;
A14: i = (w * w2) * w3 by A8, A11, XXREAL_3:77;
w * w2 in F ** G by A9, A12;
hence i in (F ** G) ** H by A13, A14; :: thesis: verum