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; :: thesis: verum

( 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; :: thesis: verum