set T = n -VectSp_over F_Real;

set TR = TOP-REAL n;

reconsider B = MX2FinS (1. (F_Real,n)) as OrdBasis of n -VectSp_over F_Real by MATRLIN2:45;

A1: the carrier of (n -VectSp_over F_Real) = REAL n by MATRIX13:102

.= the carrier of (TOP-REAL n) by EUCLID:22 ;

then reconsider F = f as Function of (n -VectSp_over F_Real),(n -VectSp_over F_Real) ;

len B = n by MATRTOP1:19;

then reconsider A = AutMt (F,B,B) as Matrix of n,F_Real ;

take A ; :: thesis: f = Mx2Tran A

Mx2Tran A = Mx2Tran ((AutMt (F,B,B)),B,B) by MATRTOP1:20

.= f by A5, A4, MATRLIN2:34 ;

hence f = Mx2Tran A ; :: thesis: verum

set TR = TOP-REAL n;

reconsider B = MX2FinS (1. (F_Real,n)) as OrdBasis of n -VectSp_over F_Real by MATRLIN2:45;

A1: the carrier of (n -VectSp_over F_Real) = REAL n by MATRIX13:102

.= the carrier of (TOP-REAL n) by EUCLID:22 ;

then reconsider F = f as Function of (n -VectSp_over F_Real),(n -VectSp_over F_Real) ;

now :: thesis: for v1, v2 being Vector of (n -VectSp_over F_Real) holds F . (v1 + v2) = (F . v1) + (F . v2)

then A4:
F is additive
;let v1, v2 be Vector of (n -VectSp_over F_Real); :: thesis: F . (v1 + v2) = (F . v1) + (F . v2)

reconsider P1 = v1, P2 = v2, FP1 = F . v1, FP2 = F . v2 as Element of n -tuples_on the carrier of F_Real by MATRIX13:102;

A2: ( @ (@ FP1) = FP1 & @ (@ FP2) = FP2 ) ;

reconsider p1 = v1, p2 = v2 as Point of (TOP-REAL n) by A1;

A3: ( @ (@ P1) = P1 & @ (@ P2) = P2 ) ;

v1 + v2 = P1 + P2 by MATRIX13:102

.= p1 + p2 by A3, MATRTOP1:1 ;

hence F . (v1 + v2) = (f . p1) + (f . p2) by VECTSP_1:def 20

.= FP1 + FP2 by A2, MATRTOP1:1

.= (F . v1) + (F . v2) by MATRIX13:102 ;

:: thesis: verum

end;reconsider P1 = v1, P2 = v2, FP1 = F . v1, FP2 = F . v2 as Element of n -tuples_on the carrier of F_Real by MATRIX13:102;

A2: ( @ (@ FP1) = FP1 & @ (@ FP2) = FP2 ) ;

reconsider p1 = v1, p2 = v2 as Point of (TOP-REAL n) by A1;

A3: ( @ (@ P1) = P1 & @ (@ P2) = P2 ) ;

v1 + v2 = P1 + P2 by MATRIX13:102

.= p1 + p2 by A3, MATRTOP1:1 ;

hence F . (v1 + v2) = (f . p1) + (f . p2) by VECTSP_1:def 20

.= FP1 + FP2 by A2, MATRTOP1:1

.= (F . v1) + (F . v2) by MATRIX13:102 ;

:: thesis: verum

len B = n by MATRTOP1:19;

then reconsider A = AutMt (F,B,B) as Matrix of n,F_Real ;

take A ; :: thesis: f = Mx2Tran A

now :: thesis: for r being Scalar of F_Real

for v being Vector of (n -VectSp_over F_Real) holds F . (r * v) = r * (F . v)

then A5:
F is homogeneous
by MOD_2:def 2;for v being Vector of (n -VectSp_over F_Real) holds F . (r * v) = r * (F . v)

let r be Scalar of F_Real; :: thesis: for v being Vector of (n -VectSp_over F_Real) holds F . (r * v) = r * (F . v)

let v be Vector of (n -VectSp_over F_Real); :: thesis: F . (r * v) = r * (F . v)

reconsider p = v as Point of (TOP-REAL n) by A1;

reconsider P = v, FP = F . v as Element of n -tuples_on the carrier of F_Real by MATRIX13:102;

r * v = r * P by MATRIX13:102

.= r * p by MATRIXR1:17 ;

hence F . (r * v) = r * (f . p) by TOPREAL9:def 4

.= r * FP by MATRIXR1:17

.= r * (F . v) by MATRIX13:102 ;

:: thesis: verum

end;let v be Vector of (n -VectSp_over F_Real); :: thesis: F . (r * v) = r * (F . v)

reconsider p = v as Point of (TOP-REAL n) by A1;

reconsider P = v, FP = F . v as Element of n -tuples_on the carrier of F_Real by MATRIX13:102;

r * v = r * P by MATRIX13:102

.= r * p by MATRIXR1:17 ;

hence F . (r * v) = r * (f . p) by TOPREAL9:def 4

.= r * FP by MATRIXR1:17

.= r * (F . v) by MATRIX13:102 ;

:: thesis: verum

Mx2Tran A = Mx2Tran ((AutMt (F,B,B)),B,B) by MATRTOP1:20

.= f by A5, A4, MATRLIN2:34 ;

hence f = Mx2Tran A ; :: thesis: verum