theorem :: NDIFF11:15

for m, n being non zero Element of NAT ex f being Function of [:(REAL-NS m),(REAL-NS n):],(REAL-NS (m + n)) st
( f is one-to-one & f is onto & ( for x being Element of REAL m
for y being Element of REAL n holds f . (x,y) = x ^ y ) & ( for u, v being Point of [:(REAL-NS m),(REAL-NS n):] holds f . (u + v) = (f . u) + (f . v) ) & ( for u being Point of [:(REAL-NS m),(REAL-NS n):]
for r being Real holds f . (r * u) = r * (f . u) ) & f . (0. [:(REAL-NS m),(REAL-NS n):]) = 0. (REAL-NS (m + n)) & ( for u being Point of [:(REAL-NS m),(REAL-NS n):] holds ||.(f . u).|| = ||.u.|| ) )