theorem Th32: :: ANPROJ_8:38

for k, m being Nat
for M being Matrix of k,m,F_Real holds Mx2Tran M is Function of (RLSp2RVSp (TOP-REAL k)),(RLSp2RVSp (TOP-REAL m))