let V be finite-dimensional RealNormSpace; :: thesis: ( dim V <> 0 implies ex S being LinearOperator of V,(REAL-NS (dim V)) ex W being finite-dimensional VectSp of F_Real ex b being OrdBasis of W st
( W = RLSp2RVSp V & S is bijective & ( for x being Element of W holds S . x = x |-- b ) ) )
assume A1: dim V <> 0 ; :: thesis: ex S being LinearOperator of V,(REAL-NS (dim V)) ex W being finite-dimensional VectSp of F_Real ex b being OrdBasis of W st
( W = RLSp2RVSp V & S is bijective & ( for x being Element of W holds S . x = x |-- b ) )
A2: ( RLSp2RVSp V is finite-dimensional & dim (RLSp2RVSp V) = dim V ) by REAL_NS2:81;
reconsider W = RLSp2RVSp V as finite-dimensional VectSp of F_Real ;
set b = the OrdBasis of W;
consider T being linear-transformation of W,((dim V) -VectSp_over F_Real) such that
A3: ( T is bijective & ( for x being Element of W holds T . x = x |-- the OrdBasis of W ) ) by A2, REAL_NS2:63;
(dim V) -VectSp_over F_Real = RLSp2RVSp (RealVectSpace (Seg (dim V))) by A1, REAL_NS2:83;
then reconsider S = T as LinearOperator of V,(RealVectSpace (Seg (dim V))) by REAL_NS2:84;
A4: the carrier of (RealVectSpace (Seg (dim V))) = the carrier of (RLSp2RVSp (RealVectSpace (Seg (dim V))))
.= the carrier of ((dim V) -VectSp_over F_Real) by A1, REAL_NS2:83 ;
A5: RLSStruct(# the carrier of (REAL-NS (dim V)), the ZeroF of (REAL-NS (dim V)), the U5 of (REAL-NS (dim V)), the Mult of (REAL-NS (dim V)) #) = RLSStruct(# the carrier of (TOP-REAL (dim V)), the ZeroF of (TOP-REAL (dim V)), the U5 of (TOP-REAL (dim V)), the Mult of (TOP-REAL (dim V)) #) by REAL_NS2:1
.= RealVectSpace (Seg (dim V)) by EUCLID:def 8 ;
then reconsider K = S as Function of the carrier of V, the carrier of (REAL-NS (dim V)) ;
for x, y being Element of V holds K . (x + y) = (K . x) + (K . y)

proof

let x, y be Element of V; :: thesis: K . (x + y) = (K . x) + (K . y)
S is additive ;
hence K . (x + y) = (S . x) + (S . y)
.= (K . x) + (K . y) by Th16 ;
:: thesis: verum

end;

then A7: K is additive ;
for a being Real
for x being VECTOR of V holds K . (a * x) = a * (K . x)

proof

let a be Real; :: thesis: for x being VECTOR of V holds K . (a * x) = a * (K . x)
let x be VECTOR of V; :: thesis: K . (a * x) = a * (K . x)
thus K . (a * x) = a * (S . x) by LOPBAN_1:def 5
.= a * (K . x) by Th16 ; :: thesis: verum

end;

then K is homogeneous ;
then reconsider K = K as LinearOperator of V,(REAL-NS (dim V)) by A7;
take K ; :: thesis: ex W being finite-dimensional VectSp of F_Real ex b being OrdBasis of W st
( W = RLSp2RVSp V & K is bijective & ( for x being Element of W holds K . x = x |-- b ) )
take W ; :: thesis: ex b being OrdBasis of W st
( W = RLSp2RVSp V & K is bijective & ( for x being Element of W holds K . x = x |-- b ) )
take the OrdBasis of W ; :: thesis: ( W = RLSp2RVSp V & K is bijective & ( for x being Element of W holds K . x = x |-- the OrdBasis of W ) )
thus ( W = RLSp2RVSp V & K is bijective & ( for x being Element of W holds K . x = x |-- the OrdBasis of W ) ) by A3, A4, A5; :: thesis: verum