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:]) & ( for v being Point of [:E,F,G:] holds ||.(I . v).|| = ||.v.|| ) ) by Th15;
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; :: thesis: verum