let n, k be Nat; :: thesis:
let f be n -element real-valued FinSequence; :: thesis:
set V = n -VectSp_over F_Real;
set nk0 = (n -' k) |-> 0;
let B be OrdBasis of n -VectSp_over F_Real; :: thesis:
assume A1: B = MX2FinS (1. (F_Real,n)) ; :: thesis:
A2: len B = n by A1, MATRIX_0:def 2;
A3: f is Point of (TOP-REAL n) by Lm3;
then A4: f is Point of (n -VectSp_over F_Real) by Lm1;
A5: rng B is Basis of (n -VectSp_over F_Real) by MATRLIN:def 2;
then A6: rng B is linearly-independent by VECTSP_7:def 3;
Lin (rng B) = ModuleStr(# the carrier of (n -VectSp_over F_Real), the addF of (n -VectSp_over F_Real), the ZeroF of (n -VectSp_over F_Real), the lmult of (n -VectSp_over F_Real) #) by A5, VECTSP_7:def 3;
then A7: f in Lin (rng B) by A4;
A8: B is one-to-one by MATRLIN:def 2;
reconsider F = f as Point of (n -VectSp_over F_Real) by A3, Lm1;
A9: len f = n by CARD_1:def 7;

per cases ;

suppose A10: k >= n ; :: thesis:

then n - k <= 0 by XREAL_1:47;
then n -' k = 0 by XREAL_0:def 2;
then A11: (n -' k) |-> 0 = {} ;
f | k = f by A9, A10, FINSEQ_1:58;
hence ( f in Lin (rng (B | k)) iff f = (f | k) ^ ((n -' k) |-> 0) ) by A2, A7, A10, A11, FINSEQ_1:34, FINSEQ_1:58; :: thesis:

end;

suppose A12: k < n ; :: thesis:

then A13: len (f | k) = k by A9, FINSEQ_1:59;
A14: len ((n -' k) |-> 0) = n -' k by CARD_1:def 7;
consider KL being Linear_Combination of n -VectSp_over F_Real such that
A15: F = Sum KL and
A16: Carrier KL c= rng B and
A17: for k being Nat st 1 <= k & k <= len (F |-- B) holds
(F |-- B) /. k = KL . (B /. k) by MATRLIN:def 7;
reconsider KL = KL as Linear_Combination of rng B by A16, VECTSP_6:def 4;
A18: F |-- B = F by A1, A2, MATRLIN2:46;
n -' k = n - k by A12, XREAL_1:233;
then len ((f | k) ^ ((n -' k) |-> 0)) = k + (n - k) by A13, A14, FINSEQ_1:22;
then A19: dom ((f | k) ^ ((n -' k) |-> 0)) = dom f by A9, FINSEQ_3:29;

hereby :: thesis:

assume f in Lin (rng (B | k)) ; :: thesis:
then consider L being Linear_Combination of rng (B | k) such that
A20: Sum L = f by VECTSP_7:7;
reconsider L1 = L as Linear_Combination of rng B by RELAT_1:70, VECTSP_6:4;
A21: KL - L1 is Linear_Combination of rng B by VECTSP_6:42;
Sum (KL - L1) = (Sum KL) - (Sum L1) by VECTSP_6:47
.= 0. (n -VectSp_over F_Real) by A15, A20, VECTSP_1:19 ;
then Carrier (KL - L1) = {} by A6, A21, VECTSP_7:def 1;
then A22: ZeroLC (n -VectSp_over F_Real) = KL - L1 by VECTSP_6:def 3
.= KL + (- L1) by VECTSP_6:def 11
.= (- L1) + KL by VECTSP_6:25 ;
reconsider M1 = - (1. F_Real) as Element of F_Real ;
A23: Carrier L c= rng (B | k) by VECTSP_6:def 4;
L1 = - (- L1) ;
then A24: KL = L1 by A22, VECTSP_6:37;

now :: thesis:

let i be Nat; :: thesis:
assume A25: i in dom f ; :: thesis:

per cases by A13, A19, A25, FINSEQ_1:25;

suppose A26: i in dom (f | k) ; :: thesis:

then (f | k) . i = f . i by FUNCT_1:47;
hence ((f | k) ^ ((n -' k) |-> 0)) . i = f . i by A26, FINSEQ_1:def 7; :: thesis:

end;

suppose A27: ex j being Nat st
( j in dom ((n -' k) |-> 0) & i = k + j ) ; :: thesis:

A28: i in dom B by A9, A2, A25, FINSEQ_3:29;
then A29: B /. i = B . i by PARTFUN1:def 6;
consider j being Nat such that
A30: j in dom ((n -' k) |-> 0) and
A31: i = k + j by A27;
A32: 1 <= j by A30, FINSEQ_3:25;
not B . i in rng (B | k)

proof

assume B . i in rng (B | k) ; :: thesis:
then consider x being object such that
A33: x in dom (B | k) and
A34: (B | k) . x = B . i by FUNCT_1:def 3;
( B . x = B . i & x in dom B ) by A33, A34, FUNCT_1:47, RELAT_1:57;
then A35: i = x by A8, A28, FUNCT_1:def 4;
x in Seg k by A33, RELAT_1:57;
then A36: i <= k by A35, FINSEQ_1:1;
i >= k + 1 by A31, A32, XREAL_1:6;
hence contradiction by A36, NAT_1:13; :: thesis:

end;

then A37: not B . i in Carrier L by A23;
( 1 <= i & i <= n ) by A9, A25, FINSEQ_3:25;
then A38: (F |-- B) /. i = KL . (B /. i) by A9, A18, A17;
f . i = (F |-- B) /. i by A18, A25, PARTFUN1:def 6;
hence f . i = 0. F_Real by A24, A38, A29, A37, VECTSP_6:2
.= ((n -' k) |-> 0) . j
.= ((f | k) ^ ((n -' k) |-> 0)) . i by A13, A30, A31, FINSEQ_1:def 7 ;
:: thesis:

end;

end;

end;

hence (f | k) ^ ((n -' k) |-> 0) = f by A19, FINSEQ_1:13; :: thesis:

end;

assume A39: (f | k) ^ ((n -' k) |-> 0) = f ; :: thesis:
Carrier KL c= rng (B | k)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A40: x in Carrier KL ; :: thesis:
Carrier KL c= rng B by VECTSP_6:def 4;
then consider i being object such that
A41: i in dom B and
A42: B . i = x by A40, FUNCT_1:def 3;
reconsider i = i as Element of NAT by A41;
A43: B /. i = B . i by A41, PARTFUN1:def 6;
A44: dom B = dom f by A9, A2, FINSEQ_3:29;
assume A45: not x in rng (B | k) ; :: thesis:
not i in Seg k

proof

assume i in Seg k ; :: thesis:
then A46: i in dom (B | k) by A41, RELAT_1:57;
then (B | k) . i = B . i by FUNCT_1:47;
hence contradiction by A42, A45, A46, FUNCT_1:def 3; :: thesis:

end;

then not i in dom (f | k) by A13, FINSEQ_1:def 3;
then consider j being Nat such that
A47: j in dom ((n -' k) |-> 0) and
A48: i = k + j by A13, A19, A41, A44, FINSEQ_1:25;
A49: ((n -' k) |-> 0) . j = 0 ;
A50: ( 1 <= i & i <= n ) by A2, A41, FINSEQ_3:25;
(F |-- B) /. i = (F |-- B) . i by A18, A41, A44, PARTFUN1:def 6;
then KL . (B /. i) = f . i by A9, A18, A17, A50
.= 0. F_Real by A13, A39, A47, A48, A49, FINSEQ_1:def 7 ;
hence contradiction by A40, A42, A43, VECTSP_6:2; :: thesis:

end;

then KL is Linear_Combination of rng (B | k) by VECTSP_6:def 4;
hence f in Lin (rng (B | k)) by A15, VECTSP_7:7; :: thesis:

end;

end;