let V be finite-dimensional RealLinearSpace; :: thesis: for b being OrdBasis of RLSp2RVSp V st dim V <> 0 holds
ex S being LinearOperator of V,(REAL-NS (dim V)) st
( S is bijective & ( for x being Element of (RLSp2RVSp V) holds S . x = x |-- b ) )
let b be OrdBasis of RLSp2RVSp V; :: thesis: ( dim V <> 0 implies ex S being LinearOperator of V,(REAL-NS (dim V)) st
( S is bijective & ( for x being Element of (RLSp2RVSp V) holds S . x = x |-- b ) ) )
assume A1: dim V <> 0 ; :: thesis: ex S being LinearOperator of V,(REAL-NS (dim V)) st
( S is bijective & ( for x being Element of (RLSp2RVSp V) holds S . x = x |-- b ) )
A2: dim (RLSp2RVSp V) = dim V by REAL_NS2:81;
set W = RLSp2RVSp V;
consider T being linear-transformation of (RLSp2RVSp V),((dim V) -VectSp_over F_Real) such that
A3: ( T is bijective & ( for x being Element of (RLSp2RVSp V) holds T . x = x |-- b ) ) 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: ( K is bijective & ( for x being Element of (RLSp2RVSp V) holds K . x = x |-- b ) )
thus ( K is bijective & ( for x being Element of (RLSp2RVSp V) holds K . x = x |-- b ) ) by A3, A4, A5; :: thesis: verum