let n be Nat; :: thesis:
let Affn be affinely-independent Subset of (TOP-REAL n); :: thesis:
let EN be Enumeration of Affn; :: thesis:
reconsider Z = 0 as Element of REAL by Lm5;
set TR = TOP-REAL n;
set A = Affn;
set V = n -VectSp_over F_Real;
set E = EN;
let A1 be Subset of (n -VectSp_over F_Real); :: thesis:
assume that
A1: Affn = A1 and
A2: 0* n in Affn and
A3: EN . (len EN) = 0* n ; :: thesis:
deffunc H₁( set ) -> Element of REAL = Z;
A4: Affin Affn = [#] (Lin Affn) by A2, Th11;
set cA = (card Affn) -' 1;
let B be OrdBasis of Lin A1; :: thesis:
assume A5: B = EN | ((card Affn) -' 1) ; :: thesis:
A6: rng B = Affn \ {(0* n)} by A2, A3, A5, Th23;
then reconsider rB = rng B as Subset of (TOP-REAL n) ;
let v be Element of (Lin A1); :: thesis:
set vB = v |-- B;
consider KV being Linear_Combination of Lin A1 such that
A7: v = Sum KV and
A8: Carrier KV c= rng B and
A9: for k being Nat st 1 <= k & k <= len (v |-- B) holds
(v |-- B) /. k = KV . (B /. k) by MATRLIN:def 7;
A10: (v |-- EN) | ((card Affn) -' 1) = (v |-- Affn) * (EN | ((card Affn) -' 1)) by RELAT_1:83;
dom (v |-- Affn) = [#] (TOP-REAL n) by FUNCT_2:def 1;
then rB c= dom (v |-- Affn) ;
then A11: len ((v |-- EN) | ((card Affn) -' 1)) = len B by A5, A10, FINSEQ_2:29;
A12: [#] (Lin A1) = [#] (Lin Affn) by A1, MATRTOP2:6;
then reconsider RB = rB as Subset of (Lin Affn) ;
reconsider KR = KV as Linear_Combination of Lin Affn by A12, MATRTOP2:11;
A13: Carrier KR = Carrier KV by MATRTOP2:12;
consider KR1 being Linear_Combination of TOP-REAL n such that
A14: Carrier KR1 = Carrier KR and
A15: Sum KR1 = Sum KR by RLVECT_5:11;
rng B c= Affn by A6, XBOOLE_1:36;
then A16: Carrier KR1 c= Affn by A8, A13, A14;
reconsider KR2 = KR1 | ([#] (Lin Affn)) as Linear_Combination of Lin Affn by MATRTOP2:10;
A17: ( Carrier KR2 = Carrier KR1 & Sum KR2 = Sum KR1 ) by A14, RLVECT_5:10;
reconsider KR1 = KR1 as Linear_Combination of Affn by A16, RLVECT_2:def 6;
reconsider ms = 1 - (sum KR1) as Element of REAL by XREAL_0:def 1;
consider KR0 being Function of the carrier of (TOP-REAL n),REAL such that
A18: KR0 . (0. (TOP-REAL n)) = ms and
A19: for u being Element of (TOP-REAL n) st u <> 0. (TOP-REAL n) holds
KR0 . u = H₁(u) from FUNCT_2:sch 6();
reconsider KR0 = KR0 as Element of Funcs ( the carrier of (TOP-REAL n),REAL) by FUNCT_2:8;

now :: thesis:

let u be VECTOR of (TOP-REAL n); :: thesis:
assume not u in {(0. (TOP-REAL n))} ; :: thesis:
then u <> 0. (TOP-REAL n) by TARSKI:def 1;
hence KR0 . u = 0 by A19; :: thesis:

end;

then reconsider KR0 = KR0 as Linear_Combination of TOP-REAL n by RLVECT_2:def 3;
Carrier KR0 c= {(0. (TOP-REAL n))}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume that
A20: x in Carrier KR0 and
A21: not x in {(0. (TOP-REAL n))} ; :: thesis:
( KR0 . x <> 0 & x <> 0. (TOP-REAL n) ) by A20, A21, RLVECT_2:19, TARSKI:def 1;
hence contradiction by A19, A20; :: thesis:

end;

then reconsider KR0 = KR0 as Linear_Combination of {(0. (TOP-REAL n))} by RLVECT_2:def 6;
A22: Carrier KR0 c= {(0. (TOP-REAL n))} by RLVECT_2:def 6;
rng B is Basis of (Lin A1) by MATRLIN:def 2;
then rng B is linearly-independent by VECTSP_7:def 3;
then rng B is linearly-independent Subset of (n -VectSp_over F_Real) by VECTSP_9:11;
then rB is linearly-independent by MATRTOP2:7;
then A23: RB is linearly-independent by RLVECT_5:15;
A24: len (v |-- B) = len B by MATRLIN:def 7;
A25: Sum KR0 = (KR0 . (0. (TOP-REAL n))) * (0. (TOP-REAL n)) by RLVECT_2:32
.= 0. (TOP-REAL n) by RLVECT_1:10 ;
A26: 0. (TOP-REAL n) = 0* n by EUCLID:66;
then {(0. (TOP-REAL n))} c= Affn by A2, ZFMISC_1:31;
then reconsider KR0 = KR0 as Linear_Combination of Affn by RLVECT_2:21;
reconsider K = KR1 + KR0 as Linear_Combination of Affn by RLVECT_2:38;
A27: sum K = (sum KR1) + (sum KR0) by RLAFFIN1:34
.= (sum KR1) + (1 - (sum KR1)) by A18, A22, RLAFFIN1:32
.= 1 ;
Sum K = (Sum KR1) + (Sum KR0) by RLVECT_3:1
.= Sum KR1 by A25, RLVECT_1:def 4
.= v by A7, A15, MATRTOP2:12 ;
then A28: v |-- Affn = K by A12, A4, A27, RLAFFIN1:def 7;

now :: thesis:

let k be Nat; :: thesis:
reconsider Bk = B /. k as Element of (TOP-REAL n) by A12, RLSUB_1:10;
assume A29: ( 1 <= k & k <= len B ) ; :: thesis:
then A30: ( (v |-- B) /. k = KV . Bk & k in dom ((v |-- EN) | ((card Affn) -' 1)) ) by A24, A9, A11, FINSEQ_3:25;
A31: k in dom B by A29, FINSEQ_3:25;
then A32: Bk = B . k by PARTFUN1:def 6;
then Bk in rng B by A31, FUNCT_1:def 3;
then Bk <> 0. (TOP-REAL n) by A6, A26, ZFMISC_1:56;
then not Bk in Carrier KR0 by A22, TARSKI:def 1;
then A33: KR0 . Bk = 0 by RLVECT_2:19;
k in dom (v |-- B) by A24, A29, FINSEQ_3:25;
then A34: (v |-- B) . k = (v |-- B) /. k by PARTFUN1:def 6;
K . Bk = (KR1 . Bk) + (KR0 . Bk) by RLVECT_2:def 10;
then K . Bk = KR2 . Bk by A12, A33, FUNCT_1:49
.= KV . Bk by A23, A8, A13, A14, A15, A17, RLVECT_5:1 ;
hence ((v |-- EN) | ((card Affn) -' 1)) . k = (v |-- B) . k by A5, A28, A10, A30, A34, A32, FUNCT_1:12; :: thesis:

end;

hence v |-- B = (v |-- EN) | ((card Affn) -' 1) by A24, A11; :: thesis: