let k be Nat; for M being Matrix of k,F_Real holds Mx2Tran M is linear-transformation of (RLSp2RVSp (TOP-REAL k)),(RLSp2RVSp (TOP-REAL k))
let M be Matrix of k,F_Real; Mx2Tran M is linear-transformation of (RLSp2RVSp (TOP-REAL k)),(RLSp2RVSp (TOP-REAL k))
reconsider M2 = Mx2Tran M as Function of (RLSp2RVSp (TOP-REAL k)),(RLSp2RVSp (TOP-REAL k)) by Th32;
A1:
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)) #)
by DUALSP01:def 2;
for x, y being Element of (RLSp2RVSp (TOP-REAL k)) holds M2 . (x + y) = (M2 . x) + (M2 . y)
then A3:
M2 is additive
;
for a being Scalar of F_Real
for x being Vector of (RLSp2RVSp (TOP-REAL k)) holds M2 . (a * x) = a * (M2 . x)
hence
Mx2Tran M is linear-transformation of (RLSp2RVSp (TOP-REAL k)),(RLSp2RVSp (TOP-REAL k))
by A3, MOD_2:def 2; verum