theorem Th7: :: NDIFF11:7

for m being non zero Element of NAT
for f being LinearOperator of (REAL-NS m),(REAL-NS m) st f is bijective holds
ex g being Lipschitzian LinearOperator of (REAL-NS m),(REAL-NS m) st
( g = f " & g is one-to-one & g is onto )