let n be Nat; :: thesis:
let x0 be Element of (RealVectSpace (Seg n)); :: thesis:
let B be Subset of (RealVectSpace (Seg n)); :: thesis:
assume A1: B = RN_Base n ; :: thesis:
A2: B = { x where x is Element of REAL n : ex i being Element of NAT st
( 1 <= i & i <= n & x = Base_FinSeq n,i ) }

proof

thus B c= { x where x is Element of REAL n : ex i being Element of NAT st
( 1 <= i & i <= n & x = Base_FinSeq n,i ) } :: according to XBOOLE_0:def 10 :: thesis:

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in B ; :: thesis:
then consider i2 being Element of NAT such that
A3: ( y = Base_FinSeq n,i2 & 1 <= i2 & i2 <= n ) by A1;
thus y in { x where x is Element of REAL n : ex i being Element of NAT st
( 1 <= i & i <= n & x = Base_FinSeq n,i ) } by A3; :: thesis:

end;

thus { x where x is Element of REAL n : ex i being Element of NAT st
( 1 <= i & i <= n & x = Base_FinSeq n,i ) } c= B :: thesis:

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in { x where x is Element of REAL n : ex i being Element of NAT st
( 1 <= i & i <= n & x = Base_FinSeq n,i ) } ; :: thesis:
then ex x being Element of REAL n st
( y = x & ex i being Element of NAT st
( 1 <= i & i <= n & x = Base_FinSeq n,i ) ) ;
hence y in B by A1; :: thesis:

end;

reconsider x1 = x0 as Element of REAL n by FINSEQ_2:111;
A5: { x where x is Element of REAL n : ex i being Element of NAT st
( 1 <= i & i <= n & x = Base_FinSeq n,i & |(x1,x)| <> 0 ) } c= B

proof

let x2 be set ; :: according to TARSKI:def 3 :: thesis:
assume x2 in { x where x is Element of REAL n : ex i being Element of NAT st
( 1 <= i & i <= n & x = Base_FinSeq n,i & |(x1,x)| <> 0 ) } ; :: thesis:
then ex x being Element of REAL n st
( x = x2 & ex i being Element of NAT st
( 1 <= i & i <= n & x = Base_FinSeq n,i & |(x1,x)| <> 0 ) ) ;
hence x2 in B by A2; :: thesis:

end;

then reconsider B0 = { x where x is Element of REAL n : ex i being Element of NAT st
( 1 <= i & i <= n & x = Base_FinSeq n,i & |(x1,x)| <> 0 ) } as Subset of (RealVectSpace (Seg n)) by XBOOLE_1:1;
A6: ( Seg n = {} implies B0 = {} )

proof

assume A7: Seg n = {} ; :: thesis:

now

assume A8: B0 <> {} ; :: thesis:
consider y being Element of B0;
y in B0 by A8;
then ex x being Element of REAL n st
( x = y & ex i being Element of NAT st
( 1 <= i & i <= n & x = Base_FinSeq n,i & |(x1,x)| <> 0 ) ) ;
hence contradiction by A7; :: thesis:

end;

hence B0 = {} ; :: thesis:

end;

defpred S₁[ set , set ] means ( $1 in B0 implies ex i being Element of NAT st
( $2 = i & 1 <= i & i <= n & $1 = Base_FinSeq n,i ) );
A9: for x being set st x in B0 holds
ex y being set st
( y in Seg n & S₁[x,y] )

proof

let x be set ; :: thesis:
assume x in B0 ; :: thesis:
then consider x2 being Element of REAL n such that
A10: ( x = x2 & ex i being Element of NAT st
( 1 <= i & i <= n & x2 = Base_FinSeq n,i & |(x1,x2)| <> 0 ) ) ;
consider i0 being Element of NAT such that
A11: ( 1 <= i0 & i0 <= n & x2 = Base_FinSeq n,i0 & |(x1,x2)| <> 0 ) by A10;
i0 in Seg n by A11, FINSEQ_1:3;
hence ex y being set st
( y in Seg n & S₁[x,y] ) by A10, A11; :: thesis:

end;

consider f being Function of B0,(Seg n) such that
A12: for x being set st x in B0 holds
S₁[x,f . x] from FUNCT_2:sch 1(A9);
set X = rng f;
for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

proof

let x1, x2 be set ; :: thesis:
assume A13: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis:
then consider i1 being Element of NAT such that
A14: ( f . x1 = i1 & 1 <= i1 & i1 <= n & x1 = Base_FinSeq n,i1 ) by A12;
ex i2 being Element of NAT st
( f . x2 = i2 & 1 <= i2 & i2 <= n & x2 = Base_FinSeq n,i2 ) by A12, A13;
hence x1 = x2 by A13, A14; :: thesis:

end;

then A15: f is one-to-one by FUNCT_1:def 8;
defpred S₂[ set , set ] means ( ( $1 in B0 implies for i being Element of NAT st 1 <= i & i <= n & $1 = Base_FinSeq n,i holds
$2 = |(x1,(Base_FinSeq n,i))| ) & ( not $1 in B0 implies $2 = 0 ) );
A16: for x being set st x in the carrier of (RealVectSpace (Seg n)) holds
ex y being set st
( y in REAL & S₂[x,y] )

proof

let x be set ; :: thesis:
assume x in the carrier of (RealVectSpace (Seg n)) ; :: thesis:

per cases ;

suppose A17: x in B0 ; :: thesis:

then consider x2 being Element of REAL n such that
A18: ( x2 = x & ex i being Element of NAT st
( 1 <= i & i <= n & x2 = Base_FinSeq n,i & |(x1,x2)| <> 0 ) ) ;
reconsider y0 = |(x1,x2)| as Element of REAL ;
for i2 being Element of NAT st 1 <= i2 & i2 <= n & x = Base_FinSeq n,i2 holds
y0 = |(x1,(Base_FinSeq n,i2))| by A18;
hence ex y being set st
( y in REAL & S₂[x,y] ) by A17; :: thesis:

end;

suppose not x in B0 ; :: thesis:

hence ex y being set st
( y in REAL & S₂[x,y] ) ; :: thesis:

end;

consider l2 being Function of the carrier of (RealVectSpace (Seg n)),REAL such that
A19: for x being set st x in the carrier of (RealVectSpace (Seg n)) holds
S₂[x,l2 . x] from FUNCT_2:sch 1(A16);
A20: l2 is Element of Funcs the carrier of (RealVectSpace (Seg n)),REAL by FUNCT_2:11;
for v being Element of (RealVectSpace (Seg n)) st not v in B0 holds
l2 . v = 0 by A19;
then reconsider l3 = l2 as Linear_Combination of RealVectSpace (Seg n) by A1, A5, A20, RLVECT_2:def 5;
Carrier l3 c= B0

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in Carrier l3 ; :: thesis:
then x in { v where v is Element of (RealVectSpace (Seg n)) : l3 . v <> 0 } by RLVECT_2:def 6;
then ex v being Element of (RealVectSpace (Seg n)) st
( x = v & l3 . v <> 0 ) ;
hence x in B0 by A19; :: thesis:

end;

then reconsider l0 = l3 as Linear_Combination of B0 by RLVECT_2:def 8;
A21: dom f = B0 by A6, FUNCT_2:def 1;
A22: rng (Sgm (rng f)) = rng f by FINSEQ_1:def 13;
reconsider l1 = l0 as Linear_Combination of RealVectSpace (Seg n) ;
A23: dom ((f " ) * (Sgm (rng f))) = (Sgm (rng f)) " (dom (f " )) by RELAT_1:182
.= (Sgm (rng f)) " (rng f) by A15, FUNCT_1:55
.= dom (Sgm (rng f)) by Th2, A22 ;
dom (Sgm (rng f)) = Seg (len (Sgm (rng f))) by FINSEQ_1:def 3;
then A24: (f " ) * (Sgm (rng f)) is FinSequence by A23, FINSEQ_1:def 2;
A25: rng ((f " ) * (Sgm (rng f))) c= rng (f " ) by RELAT_1:45;
rng (f " ) = B0 by A15, A21, FUNCT_1:55;
then rng ((f " ) * (Sgm (rng f))) c= the carrier of (RealVectSpace (Seg n)) by A25, XBOOLE_1:1;
then reconsider F0 = (f " ) * (Sgm (rng f)) as FinSequence of the carrier of (RealVectSpace (Seg n)) by A24, FINSEQ_1:def 4;
A26: dom (f " ) = rng f by A15, FUNCT_1:55;
reconsider rf = rng f as finite set ;
A27: dom (ProjFinSeq x1) = Seg (len (ProjFinSeq x1)) by FINSEQ_1:def 3
.= Seg n by Def13 ;
A28: dom ((ProjFinSeq x1) * (Sgm (rng f))) = (Sgm (rng f)) " (dom (ProjFinSeq x1)) by RELAT_1:182
.= dom (Sgm (rng f)) by A27, Th2, A22 ;
dom (Sgm (rng f)) = Seg (len (Sgm (rng f))) by FINSEQ_1:def 3;
then A29: (ProjFinSeq x1) * (Sgm (rng f)) is FinSequence by A28, FINSEQ_1:def 2;
A30: rng ((ProjFinSeq x1) * (Sgm (rng f))) c= rng (ProjFinSeq x1) by RELAT_1:45;
c1: REAL n = the carrier of (RealVectSpace (Seg n)) by FINSEQ_2:111;
rng (ProjFinSeq x1) c= REAL n ;
then rng ((ProjFinSeq x1) * (Sgm (rng f))) c= REAL n by A30, XBOOLE_1:1;
then reconsider F2 = (ProjFinSeq x1) * (Sgm (rng f)) as FinSequence of the carrier of (RealVectSpace (Seg n)) by c1, A29, FINSEQ_1:def 4;
reconsider F3 = F2 as FinSequence of REAL n by FINSEQ_2:111;
A31: Sgm (rng f) is one-to-one by FINSEQ_3:99;
A32: for i3 being Element of NAT st i3 in dom (ProjFinSeq x1) & not i3 in rng (Sgm (rng f)) holds
(ProjFinSeq x1) . i3 = 0* n

proof

let i3 be Element of NAT ; :: thesis:
assume A33: ( i3 in dom (ProjFinSeq x1) & not i3 in rng (Sgm (rng f)) ) ; :: thesis:
then A34: not i3 in rng f by FINSEQ_1:def 13;
A35: i3 in Seg (len (ProjFinSeq x1)) by A33, FINSEQ_1:def 3;
len (ProjFinSeq x1) = n by Def13;
then A36: ( 1 <= i3 & i3 <= n ) by A35, FINSEQ_1:3;
then A37: (ProjFinSeq x1) . i3 = |(x1,(Base_FinSeq n,i3))| * (Base_FinSeq n,i3) by Def13;

now

assume |(x1,(Base_FinSeq n,i3))| <> 0 ; :: thesis:
then A38: Base_FinSeq n,i3 in B0 by A36;
then consider i5 being Element of NAT such that
A39: ( f . (Base_FinSeq n,i3) = i5 & 1 <= i5 & i5 <= n & Base_FinSeq n,i3 = Base_FinSeq n,i5 ) by A12;
A40: i3 = i5 by Th29, A39, A36;
Base_FinSeq n,i3 in dom f by A6, A38, FUNCT_2:def 1;
hence contradiction by A34, A39, A40, FUNCT_1:def 5; :: thesis:

end;

hence (ProjFinSeq x1) . i3 = 0* n by A37, EUCLID_4:3; :: thesis:

end;

A41: x0 = Sum (ProjFinSeq x1) by Th35
.= Sum F3 by A22, A27, A32, Th28, FINSEQ_3:99
.= Sum F2 by Th51 ;
dom F0 = (Sgm (rng f)) " (dom (f " )) by RELAT_1:182
.= (Sgm (rng f)) " (rng f) by A15, FUNCT_1:55
.= dom (Sgm (rng f)) by Th2, A22 ;
then A42: dom F0 = Seg (len (Sgm (rng f))) by FINSEQ_1:def 3;
A43: rng F0 = rng (f " ) by A22, A26, RELAT_1:47
.= dom f by A15, FUNCT_1:55 ;
A44: Carrier l0 c= B0 by RLVECT_2:def 8;
B0 c= Carrier l0

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A45: x in B0 ; :: thesis:
then reconsider xx = x as Element of REAL n by FINSEQ_2:111;
consider x6 being Element of REAL n such that
A46: ( x = x6 & ex i being Element of NAT st
( 1 <= i & i <= n & x6 = Base_FinSeq n,i & |(x1,x6)| <> 0 ) ) by A45;
consider i8 being Element of NAT such that
A47: ( 1 <= i8 & i8 <= n & x6 = Base_FinSeq n,i8 & |(x1,x6)| <> 0 ) by A46;
reconsider x66 = x6 as Element of (RealVectSpace (Seg n)) by FINSEQ_2:111;
l0 . x66 = |(x1,(Base_FinSeq n,i8))| by A19, A45, A46, A47;
then x in { v where v is Element of (RealVectSpace (Seg n)) : l0 . v <> 0 } by A46, A47;
hence x in Carrier l0 by RLVECT_2:def 6; :: thesis:

end;

then A48: rng F0 = Carrier l0 by A21, A43, A44, XBOOLE_0:def 10;
dom F2 = (Sgm (rng f)) " (Seg n) by A27, RELAT_1:182
.= dom (Sgm (rng f)) by Th2, A22 ;
then A49: dom F2 = Seg (len (Sgm (rng f))) by FINSEQ_1:def 3;
then A50: Seg (len F2) = Seg (len (Sgm (rng f))) by FINSEQ_1:def 3;
A51: len F2 = len (Sgm (rng f)) by A49, FINSEQ_1:def 3;
A52: len F2 = len F0 by A42, A50, FINSEQ_1:def 3;
reconsider F01 = F0 as PartFunc of NAT ,the carrier of (RealVectSpace (Seg n)) ;
for i being Element of NAT st i in dom F2 holds
F2 . i = (l0 . (F0 /. i)) * (F0 /. i)

proof

let i be Element of NAT ; :: thesis:
assume i in dom F2 ; :: thesis:
then A53: i in Seg (len F2) by FINSEQ_1:def 3;
then A54: i in dom (Sgm (rng f)) by A51, FINSEQ_1:def 3;
then (Sgm (rng f)) . i in rng (Sgm (rng f)) by FUNCT_1:def 5;
then reconsider i2 = (Sgm (rng f)) . i as Element of NAT ;
A55: i2 in rng (Sgm (rng f)) by A54, FUNCT_1:def 5;
reconsider r = Base_FinSeq n,i2 as Element of the carrier of (RealVectSpace (Seg n)) by FINSEQ_2:111;
i2 in rng f by A22, A54, FUNCT_1:def 5;
then A56: ( 1 <= i2 & i2 <= n ) by FINSEQ_1:3;
consider x2 being set such that
A57: ( x2 in dom f & f . x2 = i2 ) by A22, A55, FUNCT_1:def 5;
dom f = B0 by A6, FUNCT_2:def 1;
then reconsider r2 = x2 as Element of (RealVectSpace (Seg n)) by A57;
consider i22 being Element of NAT such that
A58: ( f . r2 = i22 & 1 <= i22 & i22 <= n & r2 = Base_FinSeq n,i22 ) by A12, A57;
Base_FinSeq n,i2 in B0 by A57, A58;
then consider x7 being Element of REAL n such that
A59: ( x7 = Base_FinSeq n,i2 & ex i7 being Element of NAT st
( 1 <= i7 & i7 <= n & x7 = Base_FinSeq n,i7 & |(x1,x7)| <> 0 ) ) ;
consider i7 being Element of NAT ;
A60: r in { x6 where x6 is Element of REAL n : ex i7 being Element of NAT st
( 1 <= i7 & i7 <= n & x6 = Base_FinSeq n,i7 & |(x1,x6)| <> 0 ) } by A59;
A61: dom f = B0 by A6, FUNCT_2:def 1;
F0 . i = (f " ) . ((Sgm (rng f)) . i) by A54, FUNCT_1:23
.= Base_FinSeq n,i2 by A15, A57, A58, FUNCT_1:54 ;
then Base_FinSeq n,i2 in rng F0 by A42, A50, A53, FUNCT_1:def 5;
then Base_FinSeq n,i2 in { v where v is Element of (RealVectSpace (Seg n)) : l0 . v <> 0 } by A48, RLVECT_2:def 6;
then consider v0 being Element of (RealVectSpace (Seg n)) such that
A62: ( Base_FinSeq n,i2 = v0 & l0 . v0 <> 0 ) ;
A63: Base_FinSeq n,i2 in B0 by A19, A62;
consider i4 being Element of NAT such that
A64: ( f . r = i4 & 1 <= i4 & i4 <= n & r = Base_FinSeq n,i4 ) by A12, A60;
A65: Sgm (rng f) is one-to-one by FINSEQ_3:99;
i4 = i2 by A64, A56, Th29;
then A66: ((Sgm (rng f)) " ) . (f . (Base_FinSeq n,i2)) = i by A54, A64, A65, FUNCT_1:54;
A67: f . (Base_FinSeq n,i2) in rng (Sgm (rng f)) by A22, A57, A58, FUNCT_1:def 5;
dom ((Sgm (rng f)) " ) = rng (Sgm (rng f)) by A65, FUNCT_1:55;
then ((Sgm (rng f)) " ) . (f . (Base_FinSeq n,i2)) in rng ((Sgm (rng f)) " ) by A67, FUNCT_1:def 5;
then A68: ((Sgm (rng f)) " ) . (f . (Base_FinSeq n,i2)) in dom (Sgm (rng f)) by A65, FUNCT_1:55;
A69: (f " ) . (f . (Base_FinSeq n,i2)) = Base_FinSeq n,i2 by A15, A61, A63, FUNCT_1:56;
then A70: (f " ) . ((Sgm (rng f)) . (((Sgm (rng f)) " ) . (f . (Base_FinSeq n,i2)))) = Base_FinSeq n,i2 by A67, A65, FUNCT_1:57;
A71: ((f " ) * (Sgm (rng f))) . i = Base_FinSeq n,i2 by A54, A57, A58, A69, FUNCT_1:23;
l0 . (F0 /. i) = l0 . (((f " ) * (Sgm (rng f))) . i) by A42, A51, A53, PARTFUN1:def 8
.= l0 . (Base_FinSeq n,i2) by A66, A68, A70, FUNCT_1:23
.= |(x1,(Base_FinSeq n,i2))| by A19, A56, A62 ;
then (l0 . (F0 /. i)) * (F0 /. i) = |(x1,(Base_FinSeq n,i2))| * (Base_FinSeq n,i2) by A42, A51, A53, A71, PARTFUN1:def 8
.= (ProjFinSeq x1) . ((Sgm (rng f)) . i) by A56, Def13
.= ((ProjFinSeq x1) * (Sgm (rng f))) . i by A54, FUNCT_1:23 ;
hence F2 . i = (l0 . (F0 /. i)) * (F0 /. i) ; :: thesis:

end;

then A72: x1 = Sum (l0 (#) F0) by A41, A52, RLVECT_2:def 9;
Carrier l0 c= B by A5, A44, XBOOLE_1:1;
then reconsider l2 = l0 as Linear_Combination of B by RLVECT_2:def 8;
x1 = Sum l2 by A15, A31, A48, A72, RLVECT_2:def 10;
hence ex l being Linear_Combination of B st x0 = Sum l ; :: thesis: