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) ;
now :: thesis: for v1, v2 being Vector of (n -VectSp_over F_Real) holds F . (v1 + v2) = (F . v1) + (F . v2)
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;
then A4: F is additive ;
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)
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;
then A5: F is homogeneous by MOD_2:def 2;
Mx2Tran A = Mx2Tran ((AutMt (F,B,B)),B,B) by MATRTOP1:20
.= f by A5, A4, MATRLIN2:34 ;
hence f = Mx2Tran A ; :: thesis: verum