:: by Kazuhisa Nakasho , Hiroyuki Okazaki and Yasunari Shidama

::

:: Received June 30, 2021

:: Copyright (c) 2021 Association of Mizar Users

theorem Th1: :: REAL_NS2:1

for n being Nat holds RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the addF of (TOP-REAL n), the Mult of (TOP-REAL n) #) = RLSStruct(# the carrier of (REAL-NS n), the ZeroF of (REAL-NS n), the addF of (REAL-NS n), the Mult of (REAL-NS n) #)

proof end;

Lm1: for n being Nat holds the carrier of (n -VectSp_over F_Real) = the carrier of (TOP-REAL n)

proof end;

theorem :: REAL_NS2:3

for n being Nat holds TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceNorm (REAL-NS n)

proof end;

Lm2: for n being Nat holds the carrier of (n -VectSp_over F_Real) = the carrier of (TOP-REAL n)

proof end;

theorem Th7: :: REAL_NS2:7

for n being Nat

for p, q being Element of (TOP-REAL n)

for f, g being Element of (REAL-NS n) st p = f & q = g holds

p + q = f + g

for p, q being Element of (TOP-REAL n)

for f, g being Element of (REAL-NS n) st p = f & q = g holds

p + q = f + g

proof end;

theorem Th8: :: REAL_NS2:8

for n being Nat

for r being Real

for q being Element of (TOP-REAL n)

for g being Element of (REAL-NS n) st q = g holds

r * q = r * g

for r being Real

for q being Element of (TOP-REAL n)

for g being Element of (REAL-NS n) st q = g holds

r * q = r * g

proof end;

theorem Th9: :: REAL_NS2:9

for n being Nat

for q being Element of (TOP-REAL n)

for g being Element of (REAL-NS n) st q = g holds

- q = - g

for q being Element of (TOP-REAL n)

for g being Element of (REAL-NS n) st q = g holds

- q = - g

proof end;

theorem :: REAL_NS2:10

for n being Nat

for p, q being Element of (TOP-REAL n)

for f, g being Element of (REAL-NS n) st p = f & q = g holds

p - q = f - g

for p, q being Element of (TOP-REAL n)

for f, g being Element of (REAL-NS n) st p = f & q = g holds

p - q = f - g

proof end;

theorem Th11: :: REAL_NS2:11

for X being set

for n being Nat holds

( X is Linear_Combination of REAL-NS n iff X is Linear_Combination of TOP-REAL n )

for n being Nat holds

( X is Linear_Combination of REAL-NS n iff X is Linear_Combination of TOP-REAL n )

proof end;

theorem :: REAL_NS2:12

for X being set

for n being Nat holds

( X is Linear_Combination of REAL-NS n iff X is Linear_Combination of n -VectSp_over F_Real )

for n being Nat holds

( X is Linear_Combination of REAL-NS n iff X is Linear_Combination of n -VectSp_over F_Real )

proof end;

theorem :: REAL_NS2:13

for n being Nat

for Lv being Linear_Combination of TOP-REAL n

for Lr being Linear_Combination of REAL-NS n st Lr = Lv holds

Carrier Lr = Carrier Lv ;

for Lv being Linear_Combination of TOP-REAL n

for Lr being Linear_Combination of REAL-NS n st Lr = Lv holds

Carrier Lr = Carrier Lv ;

theorem :: REAL_NS2:14

for n being Nat

for Lv being Linear_Combination of n -VectSp_over F_Real

for Lr being Linear_Combination of REAL-NS n st Lr = Lv holds

Carrier Lr = Carrier Lv

for Lv being Linear_Combination of n -VectSp_over F_Real

for Lr being Linear_Combination of REAL-NS n st Lr = Lv holds

Carrier Lr = Carrier Lv

proof end;

theorem :: REAL_NS2:15

theorem :: REAL_NS2:16

theorem :: REAL_NS2:17

for n being Nat

for F being set holds

( F is FinSequence of (TOP-REAL n) iff F is FinSequence of (REAL-NS n) ) by Th4;

for F being set holds

( F is FinSequence of (TOP-REAL n) iff F is FinSequence of (REAL-NS n) ) by Th4;

theorem Th18: :: REAL_NS2:18

for n being Nat

for F being set holds

( F is Function of (TOP-REAL n),REAL iff F is Function of (REAL-NS n),REAL )

for F being set holds

( F is Function of (TOP-REAL n),REAL iff F is Function of (REAL-NS n),REAL )

proof end;

theorem Th19: :: REAL_NS2:19

for n being Nat

for Fr being FinSequence of (TOP-REAL n)

for fr being Function of (TOP-REAL n),REAL

for Fv being FinSequence of (REAL-NS n)

for fv being Function of (REAL-NS n),REAL st fr = fv & Fr = Fv holds

fr (#) Fr = fv (#) Fv

for Fr being FinSequence of (TOP-REAL n)

for fr being Function of (TOP-REAL n),REAL

for Fv being FinSequence of (REAL-NS n)

for fv being Function of (REAL-NS n),REAL st fr = fv & Fr = Fv holds

fr (#) Fr = fv (#) Fv

proof end;

theorem :: REAL_NS2:20

for n being Nat

for F being FinSequence of (REAL-NS n)

for fr being Function of (REAL-NS n),REAL

for Fv being FinSequence of (n -VectSp_over F_Real)

for fv being Function of (n -VectSp_over F_Real),F_Real st fr = fv & F = Fv holds

fr (#) F = fv (#) Fv

for F being FinSequence of (REAL-NS n)

for fr being Function of (REAL-NS n),REAL

for Fv being FinSequence of (n -VectSp_over F_Real)

for fv being Function of (n -VectSp_over F_Real),F_Real st fr = fv & F = Fv holds

fr (#) F = fv (#) Fv

proof end;

theorem Th21: :: REAL_NS2:21

for n being Nat

for Ft being FinSequence of (TOP-REAL n)

for Fr being FinSequence of (REAL-NS n) st Ft = Fr holds

Sum Ft = Sum Fr

for Ft being FinSequence of (TOP-REAL n)

for Fr being FinSequence of (REAL-NS n) st Ft = Fr holds

Sum Ft = Sum Fr

proof end;

theorem :: REAL_NS2:22

for n being Nat

for F being FinSequence of (REAL-NS n)

for Fv being FinSequence of (n -VectSp_over F_Real) st Fv = F holds

Sum F = Sum Fv

for F being FinSequence of (REAL-NS n)

for Fv being FinSequence of (n -VectSp_over F_Real) st Fv = F holds

Sum F = Sum Fv

proof end;

theorem Th23: :: REAL_NS2:23

for n being Nat

for Lr being Linear_Combination of REAL-NS n

for Lt being Linear_Combination of TOP-REAL n st Lr = Lt holds

Sum Lr = Sum Lt

for Lr being Linear_Combination of REAL-NS n

for Lt being Linear_Combination of TOP-REAL n st Lr = Lt holds

Sum Lr = Sum Lt

proof end;

theorem :: REAL_NS2:24

for n being Nat

for Lv being Linear_Combination of n -VectSp_over F_Real

for Lr being Linear_Combination of REAL-NS n st Lr = Lv holds

Sum Lr = Sum Lv

for Lv being Linear_Combination of n -VectSp_over F_Real

for Lr being Linear_Combination of REAL-NS n st Lr = Lv holds

Sum Lr = Sum Lv

proof end;

theorem Th25: :: REAL_NS2:25

for n being Nat

for Ar being Subset of (REAL-NS n)

for At being Subset of (TOP-REAL n) st Ar = At holds

for X being object holds

( X is Linear_Combination of Ar iff X is Linear_Combination of At )

for Ar being Subset of (REAL-NS n)

for At being Subset of (TOP-REAL n) st Ar = At holds

for X being object holds

( X is Linear_Combination of Ar iff X is Linear_Combination of At )

proof end;

theorem Th26: :: REAL_NS2:26

for n being Nat

for Ar being Subset of (REAL-NS n)

for At being Subset of (TOP-REAL n) st Ar = At holds

[#] (Lin Ar) = [#] (Lin At)

for Ar being Subset of (REAL-NS n)

for At being Subset of (TOP-REAL n) st Ar = At holds

[#] (Lin Ar) = [#] (Lin At)

proof end;

theorem :: REAL_NS2:27

for n being Nat

for Af being Subset of (n -VectSp_over F_Real)

for Ar being Subset of (REAL-NS n) st Af = Ar holds

[#] (Lin Ar) = [#] (Lin Af)

for Af being Subset of (n -VectSp_over F_Real)

for Ar being Subset of (REAL-NS n) st Af = Ar holds

[#] (Lin Ar) = [#] (Lin Af)

proof end;

theorem Th28: :: REAL_NS2:28

for n being Nat

for Ar being Subset of (REAL-NS n)

for At being Subset of (TOP-REAL n) st Ar = At holds

( Ar is linearly-independent iff At is linearly-independent )

for Ar being Subset of (REAL-NS n)

for At being Subset of (TOP-REAL n) st Ar = At holds

( Ar is linearly-independent iff At is linearly-independent )

proof end;

theorem :: REAL_NS2:29

for n being Nat

for Af being Subset of (n -VectSp_over F_Real)

for Ar being Subset of (REAL-NS n) st Af = Ar holds

( Af is linearly-independent iff Ar is linearly-independent )

for Af being Subset of (n -VectSp_over F_Real)

for Ar being Subset of (REAL-NS n) st Af = Ar holds

( Af is linearly-independent iff Ar is linearly-independent )

proof end;

theorem Th30: :: REAL_NS2:30

for n being Nat

for X being object holds

( X is Subspace of REAL-NS n iff X is Subspace of TOP-REAL n )

for X being object holds

( X is Subspace of REAL-NS n iff X is Subspace of TOP-REAL n )

proof end;

theorem :: REAL_NS2:31

for n being Nat

for X being set

for U being Subspace of REAL-NS n

for W being Subspace of n -VectSp_over F_Real st [#] U = [#] W holds

( X is Linear_Combination of U iff X is Linear_Combination of W )

for X being set

for U being Subspace of REAL-NS n

for W being Subspace of n -VectSp_over F_Real st [#] U = [#] W holds

( X is Linear_Combination of U iff X is Linear_Combination of W )

proof end;

theorem Th32: :: REAL_NS2:32

for n being Nat

for F being one-to-one FinSequence of (REAL-NS n) st rng F is linearly-independent holds

ex M being Matrix of n,F_Real st

( M is invertible & M | (len F) = F )

for F being one-to-one FinSequence of (REAL-NS n) st rng F is linearly-independent holds

ex M being Matrix of n,F_Real st

( M is invertible & M | (len F) = F )

proof end;

theorem Th33: :: REAL_NS2:33

for n being Nat

for M being Matrix of n,F_Real

for N being Matrix of n,REAL st N = MXF2MXR M holds

( M is invertible iff N is invertible )

for M being Matrix of n,F_Real

for N being Matrix of n,REAL st N = MXF2MXR M holds

( M is invertible iff N is invertible )

proof end;

theorem :: REAL_NS2:35

for n being Nat

for F being one-to-one FinSequence of (REAL-NS n) st rng F is linearly-independent holds

ex M being Matrix of n,REAL st

( M is invertible & M | (len F) = F )

for F being one-to-one FinSequence of (REAL-NS n) st rng F is linearly-independent holds

ex M being Matrix of n,REAL st

( M is invertible & M | (len F) = F )

proof end;

theorem :: REAL_NS2:36

for n being Nat

for F being one-to-one FinSequence of (REAL-NS n) st rng F is linearly-independent holds

for B being OrdBasis of n -VectSp_over F_Real st B = MX2FinS (1. (F_Real,n)) holds

for M being Matrix of n,F_Real st M is invertible & M | (len F) = F holds

(Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) = [#] (Lin (rng F))

for F being one-to-one FinSequence of (REAL-NS n) st rng F is linearly-independent holds

for B being OrdBasis of n -VectSp_over F_Real st B = MX2FinS (1. (F_Real,n)) holds

for M being Matrix of n,F_Real st M is invertible & M | (len F) = F holds

(Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) = [#] (Lin (rng F))

proof end;

theorem :: REAL_NS2:37

for n being Nat

for A, B being linearly-independent Subset of (REAL-NS n) st card A = card B holds

ex M being Matrix of n,F_Real st

( M is invertible & (Mx2Tran M) .: ([#] (Lin A)) = [#] (Lin B) )

for A, B being linearly-independent Subset of (REAL-NS n) st card A = card B holds

ex M being Matrix of n,F_Real st

( M is invertible & (Mx2Tran M) .: ([#] (Lin A)) = [#] (Lin B) )

proof end;

theorem :: REAL_NS2:38

for n, m being Nat

for M being Matrix of n,m,F_Real

for A being linearly-independent Subset of (REAL-NS n) st the_rank_of M = n holds

(Mx2Tran M) .: A is linearly-independent

for M being Matrix of n,m,F_Real

for A being linearly-independent Subset of (REAL-NS n) st the_rank_of M = n holds

(Mx2Tran M) .: A is linearly-independent

proof end;

theorem Th39: :: REAL_NS2:39

for n being Nat

for p being Element of (TOP-REAL n)

for f being Element of (REAL-NS n)

for H being Subset of (TOP-REAL n)

for I being Subset of (REAL-NS n) st p = f & H = I holds

p + H = f + I

for p being Element of (TOP-REAL n)

for f being Element of (REAL-NS n)

for H being Subset of (TOP-REAL n)

for I being Subset of (REAL-NS n) st p = f & H = I holds

p + H = f + I

proof end;

theorem Th40: :: REAL_NS2:40

for n being Nat

for Ar being Subset of (REAL-NS n)

for At being Subset of (TOP-REAL n) st Ar = At holds

( Ar is Affine iff At is Affine )

for Ar being Subset of (REAL-NS n)

for At being Subset of (TOP-REAL n) st Ar = At holds

( Ar is Affine iff At is Affine )

proof end;

theorem Th41: :: REAL_NS2:41

for n being Nat

for X being set holds

( X is affinely-independent Subset of (REAL-NS n) iff X is affinely-independent Subset of (TOP-REAL n) )

for X being set holds

( X is affinely-independent Subset of (REAL-NS n) iff X is affinely-independent Subset of (TOP-REAL n) )

proof end;

theorem :: REAL_NS2:42

for n, m being Nat

for M being Matrix of n,m,F_Real

for A being affinely-independent Subset of (REAL-NS n) st the_rank_of M = n holds

(Mx2Tran M) .: A is affinely-independent

for M being Matrix of n,m,F_Real

for A being affinely-independent Subset of (REAL-NS n) st the_rank_of M = n holds

(Mx2Tran M) .: A is affinely-independent

proof end;

theorem Th43: :: REAL_NS2:43

for n being Nat

for Ar being Subset of (REAL-NS n)

for At being Subset of (TOP-REAL n) st Ar = At holds

Affin Ar = Affin At

for Ar being Subset of (REAL-NS n)

for At being Subset of (TOP-REAL n) st Ar = At holds

Affin Ar = Affin At

proof end;

theorem Th44: :: REAL_NS2:44

for n being Nat

for L being Linear_Combination of REAL-NS n

for S being Linear_Combination of TOP-REAL n st L = S holds

sum L = sum S

for L being Linear_Combination of REAL-NS n

for S being Linear_Combination of TOP-REAL n st L = S holds

sum L = sum S

proof end;

theorem Th45: :: REAL_NS2:45

for n being Nat

for Ar being Subset of (REAL-NS n)

for At being Subset of (TOP-REAL n)

for v being Element of (REAL-NS n)

for w being Element of (TOP-REAL n) st Ar = At & v = w & v in Affin Ar & Ar is affinely-independent holds

v |-- Ar = w |-- At

for Ar being Subset of (REAL-NS n)

for At being Subset of (TOP-REAL n)

for v being Element of (REAL-NS n)

for w being Element of (TOP-REAL n) st Ar = At & v = w & v in Affin Ar & Ar is affinely-independent holds

v |-- Ar = w |-- At

proof end;

theorem :: REAL_NS2:46

for n, m being Nat

for M being Matrix of n,m,F_Real

for A being affinely-independent Subset of (REAL-NS n) st the_rank_of M = n holds

for v being Element of (REAL-NS n) st v in Affin A holds

( (Mx2Tran M) . v in Affin ((Mx2Tran M) .: A) & ( for f being b_{1} -element real-valued FinSequence holds (v |-- A) . f = (((Mx2Tran M) . v) |-- ((Mx2Tran M) .: A)) . ((Mx2Tran M) . f) ) )

for M being Matrix of n,m,F_Real

for A being affinely-independent Subset of (REAL-NS n) st the_rank_of M = n holds

for v being Element of (REAL-NS n) st v in Affin A holds

( (Mx2Tran M) . v in Affin ((Mx2Tran M) .: A) & ( for f being b

proof end;

theorem :: REAL_NS2:47

for n, m being Nat

for M being Matrix of n,m,F_Real

for A being linearly-independent Subset of (REAL-NS m) st the_rank_of M = n holds

(Mx2Tran M) " A is linearly-independent

for M being Matrix of n,m,F_Real

for A being linearly-independent Subset of (REAL-NS m) st the_rank_of M = n holds

(Mx2Tran M) " A is linearly-independent

proof end;

theorem :: REAL_NS2:48

for n, m being Nat

for M being Matrix of n,m,F_Real

for A being affinely-independent Subset of (REAL-NS m) st the_rank_of M = n holds

(Mx2Tran M) " A is affinely-independent

for M being Matrix of n,m,F_Real

for A being affinely-independent Subset of (REAL-NS m) st the_rank_of M = n holds

(Mx2Tran M) " A is affinely-independent

proof end;

theorem Th49: :: REAL_NS2:49

for V being RealLinearSpace

for W being strict Subspace of V holds W is strict Subspace of (Omega). V

for W being strict Subspace of V holds W is strict Subspace of (Omega). V

proof end;

theorem Th50: :: REAL_NS2:50

for n being Nat

for X being set holds

( X is Basis of (n -VectSp_over F_Real) iff X is Basis of TOP-REAL n )

for X being set holds

( X is Basis of (n -VectSp_over F_Real) iff X is Basis of TOP-REAL n )

proof end;

theorem Th54: :: REAL_NS2:54

for n being non empty Nat holds

( the carrier of (TOP-REAL n) = the carrier of (n -VectSp_over F_Real) & 0. (TOP-REAL n) = 0. (n -VectSp_over F_Real) & the addF of (TOP-REAL n) = the addF of (n -VectSp_over F_Real) & the Mult of (TOP-REAL n) = the lmult of (n -VectSp_over F_Real) )

( the carrier of (TOP-REAL n) = the carrier of (n -VectSp_over F_Real) & 0. (TOP-REAL n) = 0. (n -VectSp_over F_Real) & the addF of (TOP-REAL n) = the addF of (n -VectSp_over F_Real) & the Mult of (TOP-REAL n) = the lmult of (n -VectSp_over F_Real) )

proof end;

theorem :: REAL_NS2:55

theorem :: REAL_NS2:56

theorem Th57: :: REAL_NS2:57

for n being non empty Nat

for xv being Element of (n -VectSp_over F_Real)

for xt being Element of (TOP-REAL n) st xv = xt holds

- xv = - xt

for xv being Element of (n -VectSp_over F_Real)

for xt being Element of (TOP-REAL n) st xv = xt holds

- xv = - xt

proof end;

theorem :: REAL_NS2:58

for n being non empty Nat

for xv, yv being Element of (n -VectSp_over F_Real)

for xt, yt being Element of (TOP-REAL n) st xv = xt & yv = yt holds

xv - yv = xt - yt

for xv, yv being Element of (n -VectSp_over F_Real)

for xt, yt being Element of (TOP-REAL n) st xv = xt & yv = yt holds

xv - yv = xt - yt

proof end;

theorem :: REAL_NS2:59

for n being non empty Nat

for At being Subset of (TOP-REAL n)

for Ar being Subset of (n -VectSp_over F_Real) st At = Ar holds

( the carrier of (Lin At) = the carrier of (Lin Ar) & 0. (Lin At) = 0. (Lin Ar) & the addF of (Lin At) = the addF of (Lin Ar) & the Mult of (Lin At) = the lmult of (Lin Ar) )

for At being Subset of (TOP-REAL n)

for Ar being Subset of (n -VectSp_over F_Real) st At = Ar holds

( the carrier of (Lin At) = the carrier of (Lin Ar) & 0. (Lin At) = 0. (Lin Ar) & the addF of (Lin At) = the addF of (Lin Ar) & the Mult of (Lin At) = the lmult of (Lin Ar) )

proof end;

theorem :: REAL_NS2:60

for n being Nat

for At being Subset of (TOP-REAL n)

for Ar being Subset of (REAL-NS n) st At = Ar holds

Lin At = Lin Ar

for At being Subset of (TOP-REAL n)

for Ar being Subset of (REAL-NS n) st At = Ar holds

Lin At = Lin Ar

proof end;

registration

ex b_{1} being RealNormSpace st b_{1} is finite-dimensional
end;

cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V303() RealNormSpace-like finite-dimensional for NORMSTR ;

existence ex b

proof end;

theorem Th63: :: REAL_NS2:63

for K being Field

for V being finite-dimensional VectSp of K

for b being OrdBasis of V ex T being linear-transformation of V,((dim V) -VectSp_over K) st

( T is bijective & ( for x being Element of V holds T . x = x |-- b ) )

for V being finite-dimensional VectSp of K

for b being OrdBasis of V ex T being linear-transformation of V,((dim V) -VectSp_over K) st

( T is bijective & ( for x being Element of V holds T . x = x |-- b ) )

proof end;

theorem Th64: :: REAL_NS2:64

for K being Field

for V being finite-dimensional VectSp of K ex T being linear-transformation of V,((dim V) -VectSp_over K) st T is bijective

for V being finite-dimensional VectSp of K ex T being linear-transformation of V,((dim V) -VectSp_over K) st T is bijective

proof end;

theorem :: REAL_NS2:65

for K being Field

for V, W being finite-dimensional VectSp of K holds

( dim V = dim W iff ex T being linear-transformation of V,W st T is bijective )

for V, W being finite-dimensional VectSp of K holds

( dim V = dim W iff ex T being linear-transformation of V,W st T is bijective )

proof end;

theorem :: REAL_NS2:66

theorem :: REAL_NS2:69

for V being RealLinearSpace

for F being set holds

( F is Subset of V iff F is Subset of (RLSp2RVSp V) ) ;

for F being set holds

( F is Subset of V iff F is Subset of (RLSp2RVSp V) ) ;

theorem :: REAL_NS2:70

for V being RealLinearSpace

for F being set holds

( F is FinSequence of V iff F is FinSequence of (RLSp2RVSp V) ) ;

for F being set holds

( F is FinSequence of V iff F is FinSequence of (RLSp2RVSp V) ) ;

theorem :: REAL_NS2:71

theorem Th72: :: REAL_NS2:72

for T being RealLinearSpace

for X being set holds

( X is Linear_Combination of RLSp2RVSp T iff X is Linear_Combination of T )

for X being set holds

( X is Linear_Combination of RLSp2RVSp T iff X is Linear_Combination of T )

proof end;

theorem Th73: :: REAL_NS2:73

for T being RealLinearSpace

for Lv being Linear_Combination of RLSp2RVSp T

for Lr being Linear_Combination of T st Lr = Lv holds

Carrier Lr = Carrier Lv

for Lv being Linear_Combination of RLSp2RVSp T

for Lr being Linear_Combination of T st Lr = Lv holds

Carrier Lr = Carrier Lv

proof end;

theorem Th74: :: REAL_NS2:74

for V being RealLinearSpace

for Fr being FinSequence of V

for fr being Function of V,REAL

for Fv being FinSequence of (RLSp2RVSp V)

for fv being Function of (RLSp2RVSp V),F_Real st fr = fv & Fr = Fv holds

fr (#) Fr = fv (#) Fv

for Fr being FinSequence of V

for fr being Function of V,REAL

for Fv being FinSequence of (RLSp2RVSp V)

for fv being Function of (RLSp2RVSp V),F_Real st fr = fv & Fr = Fv holds

fr (#) Fr = fv (#) Fv

proof end;

theorem :: REAL_NS2:75

for T being RealLinearSpace

for Ft being FinSequence of T

for Fr being FinSequence of (RLSp2RVSp T) st Ft = Fr holds

Sum Ft = Sum Fr ;

for Ft being FinSequence of T

for Fr being FinSequence of (RLSp2RVSp T) st Ft = Fr holds

Sum Ft = Sum Fr ;

theorem Th76: :: REAL_NS2:76

for T being RealLinearSpace

for Lv being Linear_Combination of RLSp2RVSp T

for Lr being Linear_Combination of T st Lr = Lv holds

Sum Lr = Sum Lv

for Lv being Linear_Combination of RLSp2RVSp T

for Lr being Linear_Combination of T st Lr = Lv holds

Sum Lr = Sum Lv

proof end;

theorem Th77: :: REAL_NS2:77

for T being RealLinearSpace

for Af being Subset of (RLSp2RVSp T)

for Ar being Subset of T st Af = Ar holds

[#] (Lin Ar) = [#] (Lin Af)

for Af being Subset of (RLSp2RVSp T)

for Ar being Subset of T st Af = Ar holds

[#] (Lin Ar) = [#] (Lin Af)

proof end;

theorem Th78: :: REAL_NS2:78

for T being RealLinearSpace

for Af being Subset of (RLSp2RVSp T)

for Ar being Subset of T st Af = Ar holds

( Af is linearly-independent iff Ar is linearly-independent )

for Af being Subset of (RLSp2RVSp T)

for Ar being Subset of T st Af = Ar holds

( Af is linearly-independent iff Ar is linearly-independent )

proof end;

theorem :: REAL_NS2:79

for T being RealLinearSpace

for X being set

for U being Subspace of RLSp2RVSp T

for W being Subspace of T st [#] U = [#] W holds

( X is Linear_Combination of U iff X is Linear_Combination of W )

for X being set

for U being Subspace of RLSp2RVSp T

for W being Subspace of T st [#] U = [#] W holds

( X is Linear_Combination of U iff X is Linear_Combination of W )

proof end;

theorem Th80: :: REAL_NS2:80

for W being RealLinearSpace

for X being set holds

( X is Basis of (RLSp2RVSp W) iff X is Basis of W )

for X being set holds

( X is Basis of (RLSp2RVSp W) iff X is Basis of W )

proof end;

theorem Th81: :: REAL_NS2:81

for W being RealLinearSpace st W is finite-dimensional holds

( RLSp2RVSp W is finite-dimensional & dim (RLSp2RVSp W) = dim W )

( RLSp2RVSp W is finite-dimensional & dim (RLSp2RVSp W) = dim W )

proof end;

theorem Th84: :: REAL_NS2:84

for V, W being RealLinearSpace

for X being set holds

( X is LinearOperator of V,W iff X is linear-transformation of (RLSp2RVSp V),(RLSp2RVSp W) )

for X being set holds

( X is LinearOperator of V,W iff X is linear-transformation of (RLSp2RVSp V),(RLSp2RVSp W) )

proof end;

theorem Th85: :: REAL_NS2:85

for X, Y being RealLinearSpace

for L being LinearOperator of X,Y st L is bijective holds

ex K being LinearOperator of Y,X st

( K = L " & K is one-to-one & K is onto )

for L being LinearOperator of X,Y st L is bijective holds

ex K being LinearOperator of Y,X st

( K = L " & K is one-to-one & K is onto )

proof end;

theorem Th86: :: REAL_NS2:86

for X, Y, Z being RealLinearSpace

for L being LinearOperator of X,Y

for K being LinearOperator of Y,Z holds K * L is LinearOperator of X,Z

for L being LinearOperator of X,Y

for K being LinearOperator of Y,Z holds K * L is LinearOperator of X,Z

proof end;

theorem Th87: :: REAL_NS2:87

for V, W being RealLinearSpace

for A being Subset of V

for T being LinearOperator of V,W st T is bijective holds

( A is Basis of V iff T .: A is Basis of W )

for A being Subset of V

for T being LinearOperator of V,W st T is bijective holds

( A is Basis of V iff T .: A is Basis of W )

proof end;

theorem Th88: :: REAL_NS2:88

for V being finite-dimensional RealLinearSpace

for W being RealLinearSpace st ex T being LinearOperator of V,W st T is bijective holds

( W is finite-dimensional & dim W = dim V )

for W being RealLinearSpace st ex T being LinearOperator of V,W st T is bijective holds

( W is finite-dimensional & dim W = dim V )

proof end;

theorem Th89: :: REAL_NS2:89

for V being finite-dimensional RealLinearSpace st dim V <> 0 holds

ex T being LinearOperator of V,(RealVectSpace (Seg (dim V))) st T is bijective

ex T being LinearOperator of V,(RealVectSpace (Seg (dim V))) st T is bijective

proof end;

theorem :: REAL_NS2:90

for V, W being finite-dimensional RealLinearSpace st dim V <> 0 holds

( dim V = dim W iff ex T being LinearOperator of V,W st T is bijective )

( dim V = dim W iff ex T being LinearOperator of V,W st T is bijective )

proof end;