theorem Th14: :: NDIFF11:14

for m, n being non zero Element of NAT ex f being Function of [:(REAL m),(REAL n):],(REAL (m + n)) st
( ( for x being Element of REAL m
for y being Element of REAL n holds f . (x,y) = x ^ y ) & f is one-to-one & f is onto )