consider I being Function of [:E,F,G:],(product <*E,F,G*>) such that
( I is one-to-one & I is onto )
and
A1:
for x being Point of E
for y being Point of F
for z being Point of G holds I . (x,y,z) = <*x,y,z*>
and
( ( for v, w being Point of [:E,F,G:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:E,F,G:]
for r being Real holds I . (r * v) = r * (I . v) ) & 0. (product <*E,F,G*>) = I . (0. [:E,F,G:]) )
by Th11;
A2:
I . [e,f,g] in rng I
by FUNCT_2:112;
I . (e,f,g) = <*e,f,g*>
by A1;
hence
<*e,f,g*> is Element of (product <*E,F,G*>)
by A2; verum