let n be Nat; :: thesis: for Affn being affinely-independent Subset of ()
for EN being Enumeration of Affn
for A being Subset of () st Affn = A & 0* n in Affn & EN . (len EN) = 0* n holds
for B being OrdBasis of Lin A st B = EN | ((card Affn) -' 1) holds
for v being Element of (Lin A) holds v |-- B = (v |-- EN) | ((card Affn) -' 1)

let Affn be affinely-independent Subset of (); :: thesis: for EN being Enumeration of Affn
for A being Subset of () st Affn = A & 0* n in Affn & EN . (len EN) = 0* n holds
for B being OrdBasis of Lin A st B = EN | ((card Affn) -' 1) holds
for v being Element of (Lin A) holds v |-- B = (v |-- EN) | ((card Affn) -' 1)

let EN be Enumeration of Affn; :: thesis: for A being Subset of () st Affn = A & 0* n in Affn & EN . (len EN) = 0* n holds
for B being OrdBasis of Lin A st B = EN | ((card Affn) -' 1) holds
for v being Element of (Lin A) holds v |-- B = (v |-- EN) | ((card Affn) -' 1)

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 (); :: thesis: ( Affn = A1 & 0* n in Affn & EN . (len EN) = 0* n implies for B being OrdBasis of Lin A1 st B = EN | ((card Affn) -' 1) holds
for v being Element of (Lin A1) holds v |-- B = (v |-- EN) | ((card Affn) -' 1) )

assume that
A1: Affn = A1 and
A2: 0* n in Affn and
A3: EN . (len EN) = 0* n ; :: thesis: for B being OrdBasis of Lin A1 st B = EN | ((card Affn) -' 1) holds
for v being Element of (Lin A1) holds v |-- B = (v |-- EN) | ((card Affn) -' 1)

deffunc H1( set ) -> Element of REAL = Z;
A4: Affin Affn = [#] (Lin Affn) by ;
set cA = (card Affn) -' 1;
let B be OrdBasis of Lin A1; :: thesis: ( B = EN | ((card Affn) -' 1) implies for v being Element of (Lin A1) holds v |-- B = (v |-- EN) | ((card Affn) -' 1) )
assume A5: B = EN | ((card Affn) -' 1) ; :: thesis: for v being Element of (Lin A1) holds v |-- B = (v |-- EN) | ((card Affn) -' 1)
A6: rng B = Affn \ {(0* n)} by A2, A3, A5, Th23;
then reconsider rB = rng B as Subset of () ;
let v be Element of (Lin A1); :: thesis: v |-- B = (v |-- EN) | ((card Affn) -' 1)
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) = [#] () by FUNCT_2:def 1;
then rB c= dom (v |-- Affn) ;
then A11: len ((v |-- EN) | ((card Affn) -' 1)) = len B by ;
A12: [#] (Lin A1) = [#] (Lin Affn) by ;
then reconsider RB = rB as Subset of (Lin Affn) ;
reconsider KR = KV as Linear_Combination of Lin Affn by ;
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 ;
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 ;
reconsider KR1 = KR1 as Linear_Combination of Affn by ;
reconsider ms = 1 - (sum KR1) as Element of REAL by XREAL_0:def 1;
consider KR0 being Function of the carrier of (),REAL such that
A18: KR0 . (0. ()) = ms and
A19: for u being Element of () st u <> 0. () holds
KR0 . u = H1(u) from reconsider KR0 = KR0 as Element of Funcs ( the carrier of (),REAL) by FUNCT_2:8;
now :: thesis: for u being VECTOR of () st not u in {(0. ())} holds
KR0 . u = 0
let u be VECTOR of (); :: thesis: ( not u in {(0. ())} implies KR0 . u = 0 )
assume not u in {(0. ())} ; :: thesis: KR0 . u = 0
then u <> 0. () by TARSKI:def 1;
hence KR0 . u = 0 by A19; :: thesis: verum
end;
then reconsider KR0 = KR0 as Linear_Combination of TOP-REAL n by RLVECT_2:def 3;
Carrier KR0 c= {(0. ())}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier KR0 or x in {(0. ())} )
assume that
A20: x in Carrier KR0 and
A21: not x in {(0. ())} ; :: thesis: contradiction
( KR0 . x <> 0 & x <> 0. () ) by ;
hence contradiction by A19, A20; :: thesis: verum
end;
then reconsider KR0 = KR0 as Linear_Combination of {(0. ())} by RLVECT_2:def 6;
A22: Carrier KR0 c= {(0. ())} 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 () 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. ())) * (0. ()) by RLVECT_2:32
.= 0. () by RLVECT_1:10 ;
A26: 0. () = 0* n by EUCLID:66;
then {(0. ())} c= Affn by ;
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
.= 1 ;
Sum K = (Sum KR1) + (Sum KR0) by RLVECT_3:1
.= Sum KR1 by
.= v by ;
then A28: v |-- Affn = K by ;
now :: thesis: for k being Nat st 1 <= k & k <= len B holds
((v |-- EN) | ((card Affn) -' 1)) . k = (v |-- B) . k
let k be Nat; :: thesis: ( 1 <= k & k <= len B implies ((v |-- EN) | ((card Affn) -' 1)) . k = (v |-- B) . k )
reconsider Bk = B /. k as Element of () by ;
assume A29: ( 1 <= k & k <= len B ) ; :: thesis: ((v |-- EN) | ((card Affn) -' 1)) . k = (v |-- B) . k
then A30: ( (v |-- B) /. k = KV . Bk & k in dom ((v |-- EN) | ((card Affn) -' 1)) ) by ;
A31: k in dom B by ;
then A32: Bk = B . k by PARTFUN1:def 6;
then Bk in rng B by ;
then Bk <> 0. () by ;
then not Bk in Carrier KR0 by ;
then A33: KR0 . Bk = 0 by RLVECT_2:19;
k in dom (v |-- B) by ;
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
.= KV . Bk by ;
hence ((v |-- EN) | ((card Affn) -' 1)) . k = (v |-- B) . k by ; :: thesis: verum
end;
hence v |-- B = (v |-- EN) | ((card Affn) -' 1) by ; :: thesis: verum