let k, m be Nat; :: thesis: for M being Matrix of k,m,F_Real holds Mx2Tran M is Function of (RLSp2RVSp (TOP-REAL k)),(RLSp2RVSp (TOP-REAL m))
let M be Matrix of k,m,F_Real; :: thesis: Mx2Tran M is Function of (RLSp2RVSp (TOP-REAL k)),(RLSp2RVSp (TOP-REAL m))
( RLSp2RVSp (TOP-REAL k) = ModuleStr(# the carrier of (TOP-REAL k), the addF of (TOP-REAL k), the ZeroF of (TOP-REAL k),(MultF_Real* (TOP-REAL k)) #) & RLSp2RVSp (TOP-REAL m) = ModuleStr(# the carrier of (TOP-REAL m), the addF of (TOP-REAL m), the ZeroF of (TOP-REAL m),(MultF_Real* (TOP-REAL m)) #) ) by DUALSP01:def 2;
hence Mx2Tran M is Function of (RLSp2RVSp (TOP-REAL k)),(RLSp2RVSp (TOP-REAL m)) ; :: thesis: verum