let n be Element of NAT ; :: thesis: for x0 being Element of (REAL-US n)
for B being Subset of (REAL-US n) st B = RN_Base n holds
ex l being Linear_Combination of B st x0 = Sum l
let x0 be Element of (REAL-US n); :: thesis: for B being Subset of (REAL-US n) st B = RN_Base n holds
ex l being Linear_Combination of B st x0 = Sum l
let B be Subset of (REAL-US n); :: thesis: ( B = RN_Base n implies ex l being Linear_Combination of B st x0 = Sum l )
reconsider x1 = x0 as Element of REAL n by REAL_NS1:def 6;
A1: REAL n = the carrier of (REAL-US n) by REAL_NS1:def 6;
assume A2: B = RN_Base n ; :: thesis: ex l being Linear_Combination of B st x0 = Sum l
A3: { 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

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not 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) ) } or y in B )
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: y in B
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 A2; :: thesis: verum

end;

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) ) }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in B or 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) ) } )
assume y in B ; :: thesis: 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) ) }
then ex i2 being Element of NAT st
( y = Base_FinSeq (n,i2) & 1 <= i2 & i2 <= n ) by A2;
hence 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: verum

end;

then A4: 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) ) } by A3, XBOOLE_0:def 10;
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 object ; :: according to TARSKI:def 3 :: thesis: ( not 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 ) } or x2 in B )
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: x2 in B
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 A4; :: thesis: verum

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 (REAL-US n) by XBOOLE_1:1;
defpred S₁[ object , object ] means ( $1 in B0 implies ex i being Element of NAT st
( $2 = i & 1 <= i & i <= n & $1 = Base_FinSeq (n,i) ) );
A6: for x being object st x in B0 holds
ex y being object st
( y in Seg n & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in B0 implies ex y being object st
( y in Seg n & S₁[x,y] ) )
assume x in B0 ; :: thesis: ex y being object st
( y in Seg n & S₁[x,y] )
then consider x2 being Element of REAL n such that
A7: x = x2 and
A8: 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
A9: 1 <= i0 and
A10: i0 <= n and
A11: x2 = Base_FinSeq (n,i0) and
|(x1,x2)| <> 0 by A8;
i0 in Seg n by A9, A10, FINSEQ_1:1;
hence ex y being object st
( y in Seg n & S₁[x,y] ) by A7, A9, A10, A11; :: thesis: verum

end;

consider f being Function of B0,(Seg n) such that
A12: for x being object st x in B0 holds
S₁[x,f . x] from FUNCT_2:sch 1(A6);
defpred S₂[ object , object ] 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 ) );
A13: for x being object st x in the carrier of (REAL-US n) holds
ex y being object st
( y in REAL & S₂[x,y] )

proof

let x be object ; :: thesis: ( x in the carrier of (REAL-US n) implies ex y being object st
( y in REAL & S₂[x,y] ) )
assume x in the carrier of (REAL-US n) ; :: thesis: ex y being object st
( y in REAL & S₂[x,y] )

per cases ( x in B0 or not x in B0 ) ;

suppose A14: x in B0 ; :: thesis: ex y being object st
( y in REAL & S₂[x,y] )

then consider x2 being Element of REAL n such that
A15: x2 = x and
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 A15;
hence ex y being object st
( y in REAL & S₂[x,y] ) by A14; :: thesis: verum

end;

suppose not x in B0 ; :: thesis: ex y being object st
( y in REAL & S₂[x,y] )

hence ex y being object st
( y in REAL & S₂[x,y] ) by Lm3; :: thesis: verum

end;

end;

end;

consider l2 being Function of the carrier of (REAL-US n),REAL such that
A16: for x being object st x in the carrier of (REAL-US n) holds
S₂[x,l2 . x] from FUNCT_2:sch 1(A13);
A17: l2 is Element of Funcs ( the carrier of (REAL-US n),REAL) by FUNCT_2:8;
for v being Element of (REAL-US n) st not v in B0 holds
l2 . v = 0 by A16;
then reconsider l3 = l2 as Linear_Combination of REAL-US n by A2, A5, A17, RLVECT_2:def 3;
Carrier l3 c= B0

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier l3 or x in B0 )
assume x in Carrier l3 ; :: thesis: x in B0
then x in { v where v is Element of (REAL-US n) : l3 . v <> 0 } by RLVECT_2:def 4;
then ex v being Element of (REAL-US n) st
( x = v & l3 . v <> 0 ) ;
hence x in B0 by A16; :: thesis: verum

end;

then reconsider l0 = l3 as Linear_Combination of B0 by RLVECT_2:def 6;
A18: Carrier l0 c= B0 by RLVECT_2:def 6;
then Carrier l0 c= B by A5;
then reconsider l2 = l0 as Linear_Combination of B by RLVECT_2:def 6;
A19: B0 c= Carrier l0

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B0 or x in Carrier l0 )
assume A20: x in B0 ; :: thesis: x in Carrier l0
then consider x6 being Element of REAL n such that
A21: x = x6 and
A22: ex i being Element of NAT st
( 1 <= i & i <= n & x6 = Base_FinSeq (n,i) & |(x1,x6)| <> 0 ) ;
reconsider x66 = x6 as Element of (REAL-US n) by REAL_NS1:def 6;
consider i8 being Element of NAT such that
1 <= i8 and
i8 <= n and
A23: x6 = Base_FinSeq (n,i8) and
|(x1,x6)| <> 0 by A22;
l0 . x66 = |(x1,(Base_FinSeq (n,i8)))| by A16, A20, A21, A22, A23;
then x in { v where v is Element of (REAL-US n) : l0 . v <> 0 } by A21, A22, A23;
hence x in Carrier l0 by RLVECT_2:def 4; :: thesis: verum

end;

A24: dom (Sgm (rng f)) = Seg (len (Sgm (rng f))) by FINSEQ_1:def 3;
A25: rng ((f ") * (Sgm (rng f))) c= rng (f ") by RELAT_1:26;
A26: dom (Sgm (rng f)) = Seg (len (Sgm (rng f))) by FINSEQ_1:def 3;
for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A27: x1 in dom f and
A28: x2 in dom f and
A29: f . x1 = f . x2 ; :: thesis: x1 = x2
A30: ex i2 being Element of NAT st
( f . x2 = i2 & 1 <= i2 & i2 <= n & x2 = Base_FinSeq (n,i2) ) by A12, A28;
ex i1 being Element of NAT st
( f . x1 = i1 & 1 <= i1 & i1 <= n & x1 = Base_FinSeq (n,i1) ) by A12, A27;
hence x1 = x2 by A29, A30; :: thesis: verum

end;

then A31: f is one-to-one by FUNCT_1:def 4;
A32: ( Seg n = {} implies B0 = {} )

proof

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

end;

iii: rng f is included_in_Seg by FINSEQ_1:def 13;
then A47: rng (Sgm (rng f)) = rng f by FINSEQ_1:def 14;
A34: 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: ( i3 in dom (ProjFinSeq x1) & not i3 in rng (Sgm (rng f)) implies (ProjFinSeq x1) . i3 = 0* n )
assume that
A35: i3 in dom (ProjFinSeq x1) and
A36: not i3 in rng (Sgm (rng f)) ; :: thesis: (ProjFinSeq x1) . i3 = 0* n
A37: i3 in Seg (len (ProjFinSeq x1)) by A35, FINSEQ_1:def 3;
then A38: 1 <= i3 by FINSEQ_1:1;
len (ProjFinSeq x1) = n by Def12;
then A39: i3 <= n by A37, FINSEQ_1:1;
A40: not i3 in rng f by A36, A47;

A41: now :: thesis: not |(x1,(Base_FinSeq (n,i3)))| <> 0

assume |(x1,(Base_FinSeq (n,i3)))| <> 0 ; :: thesis: contradiction
then A42: Base_FinSeq (n,i3) in B0 by A38, A39;
then consider i5 being Element of NAT such that
A43: f . (Base_FinSeq (n,i3)) = i5 and
1 <= i5 and
i5 <= n and
A44: Base_FinSeq (n,i3) = Base_FinSeq (n,i5) by A12;
A45: Base_FinSeq (n,i3) in dom f by A32, A42, FUNCT_2:def 1;
i3 = i5 by A38, A39, A44, Th24;
hence contradiction by A40, A43, A45, FUNCT_1:def 3; :: thesis: verum

end;

(ProjFinSeq x1) . i3 = |(x1,(Base_FinSeq (n,i3)))| * (Base_FinSeq (n,i3)) by A38, A39, Def12;
hence (ProjFinSeq x1) . i3 = 0* n by A41, EUCLID_4:3; :: thesis: verum

end;

A46: rng ((ProjFinSeq x1) * (Sgm (rng f))) c= REAL n ;
A48: dom f = B0 by A32, FUNCT_2:def 1;
then rng (f ") = B0 by A31, FUNCT_1:33;
then A49: rng ((f ") * (Sgm (rng f))) c= the carrier of (REAL-US n) by A25, XBOOLE_1:1;
dom ((f ") * (Sgm (rng f))) = (Sgm (rng f)) " (dom (f ")) by RELAT_1:147
.= (Sgm (rng f)) " (rng f) by A31, FUNCT_1:33
.= dom (Sgm (rng f)) by A47, Th1 ;
then (f ") * (Sgm (rng f)) is FinSequence by A26, FINSEQ_1:def 2;
then reconsider F0 = (f ") * (Sgm (rng f)) as FinSequence of the carrier of (REAL-US n) by A49, FINSEQ_1:def 4;
dom F0 = (Sgm (rng f)) " (dom (f ")) by RELAT_1:147
.= (Sgm (rng f)) " (rng f) by A31, FUNCT_1:33
.= dom (Sgm (rng f)) by A47, Th1 ;
then A50: dom F0 = Seg (len (Sgm (rng f))) by FINSEQ_1:def 3;
A51: dom (ProjFinSeq x1) = Seg (len (ProjFinSeq x1)) by FINSEQ_1:def 3
.= Seg n by Def12 ;
then dom ((ProjFinSeq x1) * (Sgm (rng f))) = (Sgm (rng f)) " (Seg n) by RELAT_1:147
.= dom (Sgm (rng f)) by A47, Th1 ;
then (ProjFinSeq x1) * (Sgm (rng f)) is FinSequence by A24, FINSEQ_1:def 2;
then reconsider F2 = (ProjFinSeq x1) * (Sgm (rng f)) as FinSequence of the carrier of (REAL-US n) by A1, A46, FINSEQ_1:def 4;
dom F2 = (Sgm (rng f)) " (Seg n) by A51, RELAT_1:147
.= dom (Sgm (rng f)) by A47, Th1 ;
then A52: dom F2 = Seg (len (Sgm (rng f))) by FINSEQ_1:def 3;
then A53: Seg (len F2) = Seg (len (Sgm (rng f))) by FINSEQ_1:def 3;
A54: len F2 = len (Sgm (rng f)) by A52, FINSEQ_1:def 3;
dom (f ") = rng f by A31, FUNCT_1:33;
then rng F0 = rng (f ") by A47, RELAT_1:28
.= dom f by A31, FUNCT_1:33 ;
then A55: rng F0 = Carrier l0 by A48, A18, A19, XBOOLE_0:def 10;
A56: for i being Nat st i in dom F2 holds
F2 . i = (l0 . (F0 /. i)) * (F0 /. i)

proof

let i be Nat; :: thesis: ( i in dom F2 implies F2 . i = (l0 . (F0 /. i)) * (F0 /. i) )
A57: Sgm (rng f) is one-to-one by iii, FINSEQ_3:92;
assume i in dom F2 ; :: thesis: F2 . i = (l0 . (F0 /. i)) * (F0 /. i)
then A58: i in Seg (len F2) by FINSEQ_1:def 3;
then A59: i in dom (Sgm (rng f)) by A54, FINSEQ_1:def 3;
then (Sgm (rng f)) . i in rng (Sgm (rng f)) by FUNCT_1:def 3;
then reconsider i2 = (Sgm (rng f)) . i as Element of NAT ;
reconsider r = Base_FinSeq (n,i2) as Element of (REAL-US n) by REAL_NS1:def 6;
i2 in rng (Sgm (rng f)) by A59, FUNCT_1:def 3;
then consider x2 being object such that
A60: x2 in dom f and
A61: f . x2 = i2 by A47, FUNCT_1:def 3;
dom f = B0 by A32, FUNCT_2:def 1;
then reconsider r2 = x2 as Element of (REAL-US n) by A60;
A62: ex i22 being Element of NAT st
( f . r2 = i22 & 1 <= i22 & i22 <= n & r2 = Base_FinSeq (n,i22) ) by A12, A60;
then consider i4 being Element of NAT such that
A63: f . r = i4 and
1 <= i4 and
i4 <= n and
A64: r = Base_FinSeq (n,i4) by A61;
A65: dom f = B0 by A32, FUNCT_2:def 1;
F0 . i = (f ") . ((Sgm (rng f)) . i) by A59, FUNCT_1:13
.= Base_FinSeq (n,i2) by A31, A60, A61, A62, FUNCT_1:32 ;
then Base_FinSeq (n,i2) in rng F0 by A50, A53, A58, FUNCT_1:def 3;
then Base_FinSeq (n,i2) in { v where v is Element of (REAL-US n) : l0 . v <> 0 } by A55, RLVECT_2:def 4;
then A66: ex v0 being Element of (REAL-US n) st
( Base_FinSeq (n,i2) = v0 & l0 . v0 <> 0 ) ;
then Base_FinSeq (n,i2) in B0 by A16;
then A67: (f ") . (f . (Base_FinSeq (n,i2))) = Base_FinSeq (n,i2) by A31, A65, FUNCT_1:34;
then A68: ((f ") * (Sgm (rng f))) . i = Base_FinSeq (n,i2) by A59, A61, A62, FUNCT_1:13;
A69: i2 in rng f by A47, A59, FUNCT_1:def 3;
then A70: 1 <= i2 by FINSEQ_1:1;
A71: i2 <= n by A69, FINSEQ_1:1;
then i4 = i2 by A70, A64, Th24;
then A72: ((Sgm (rng f)) ") . (f . (Base_FinSeq (n,i2))) = i by A59, A63, A57, FUNCT_1:32;
A73: f . (Base_FinSeq (n,i2)) in rng (Sgm (rng f)) by A47, A60, A61, A62, FUNCT_1:def 3;
then A74: (f ") . ((Sgm (rng f)) . (((Sgm (rng f)) ") . (f . (Base_FinSeq (n,i2))))) = Base_FinSeq (n,i2) by A57, A67, FUNCT_1:35;
dom ((Sgm (rng f)) ") = rng (Sgm (rng f)) by A57, FUNCT_1:33;
then ((Sgm (rng f)) ") . (f . (Base_FinSeq (n,i2))) in rng ((Sgm (rng f)) ") by A73, FUNCT_1:def 3;
then A75: ((Sgm (rng f)) ") . (f . (Base_FinSeq (n,i2))) in dom (Sgm (rng f)) by A57, FUNCT_1:33;
l0 . (F0 /. i) = l0 . (((f ") * (Sgm (rng f))) . i) by A50, A54, A58, PARTFUN1:def 6
.= l0 . (Base_FinSeq (n,i2)) by A72, A75, A74, FUNCT_1:13
.= |(x1,(Base_FinSeq (n,i2)))| by A16, A70, A71, A66 ;
then (l0 . (F0 /. i)) * (F0 /. i) = |(x1,(Base_FinSeq (n,i2)))| * (Base_FinSeq (n,i2)) by A50, A54, A58, A68, PARTFUN1:def 6
.= (ProjFinSeq x1) . ((Sgm (rng f)) . i) by A70, A71, Def12
.= ((ProjFinSeq x1) * (Sgm (rng f))) . i by A59, FUNCT_1:13 ;
hence F2 . i = (l0 . (F0 /. i)) * (F0 /. i) ; :: thesis: verum

end;

A76: Sgm (rng f) is one-to-one by iii, FINSEQ_3:92;
reconsider F3 = F2 as FinSequence of REAL n by REAL_NS1:def 6;
A77: x0 = Sum (ProjFinSeq x1) by Th30
.= Sum F3 by A47, A51, A34, iii, Th23, FINSEQ_3:92
.= Sum F2 by Th33 ;
len F2 = len F0 by A50, A53, FINSEQ_1:def 3;
then x1 = Sum (l0 (#) F0) by A77, A56, RLVECT_2:def 7;
then x1 = Sum l2 by A31, A76, A55, RLVECT_2:def 8;
hence ex l being Linear_Combination of B st x0 = Sum l ; :: thesis: verum