let k be Nat; :: thesis: 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; :: thesis: 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)

proof

let x, y be Element of (RLSp2RVSp (TOP-REAL k)); :: thesis: M2 . (x + y) = (M2 . x) + (M2 . y)
reconsider xr = x, yr = y as Element of (TOP-REAL k) by A1;
A2: x + y = xr + yr by A1;
M2 . (x + y) = ((Mx2Tran M) . xr) + ((Mx2Tran M) . yr) by A2, MATRTOP1:22
.= (M2 . x) + (M2 . y) by A1 ;
hence M2 . (x + y) = (M2 . x) + (M2 . y) ; :: thesis: verum

end;

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)

proof

let a be Scalar of F_Real; :: thesis: for x being Vector of (RLSp2RVSp (TOP-REAL k)) holds M2 . (a * x) = a * (M2 . x)
let x be Vector of (RLSp2RVSp (TOP-REAL k)); :: thesis: M2 . (a * x) = a * (M2 . x)
reconsider ra = a as Real ;
reconsider rx = x as Element of (TOP-REAL k) by A1;
reconsider X = RLSp2RVSp (TOP-REAL 3) as ModuleStr over F_Real ;
A4: a * x = a * rx

proof

MultF_Real* (TOP-REAL k) = the Mult of (TOP-REAL k) by DUALSP01:def 1;
hence a * x = a * rx by A1, RLVECT_1:def 1; :: thesis: verum

end;

a * ((Mx2Tran M) . x) = a * (M2 . x)

proof

a * (M2 . x) = the Mult of (TOP-REAL k) . (a,((Mx2Tran M) . x)) by A1, DUALSP01:def 1
.= a * ((Mx2Tran M) . rx) by RLVECT_1:def 1 ;
hence a * ((Mx2Tran M) . x) = a * (M2 . x) ; :: thesis: verum

end;

hence M2 . (a * x) = a * (M2 . x) by A4, MATRTOP1:23; :: thesis: verum

end;

hence Mx2Tran M is linear-transformation of (RLSp2RVSp (TOP-REAL k)),(RLSp2RVSp (TOP-REAL k)) by A3, MOD_2:def 2; :: thesis: verum