theorem Th14: :: PDIFF_6:14

for n, m being Nat
for f being set holds
( f is LinearOperator of m,n iff f is LinearOperator of (REAL-NS m),(REAL-NS n) )