let n be Nat; :: thesis: for Affn being affinely-independent Subset of (TOP-REAL n)
for EN being Enumeration of Affn st 0* n in Affn & EN . (len EN) = 0* n holds
( rng (EN | ((card Affn) -' 1)) = Affn \ {(0* n)} & ( for A being Subset of (n -VectSp_over F_Real) st Affn = A holds
EN | ((card Affn) -' 1) is OrdBasis of Lin A ) )
let Affn be affinely-independent Subset of (TOP-REAL n); :: thesis: for EN being Enumeration of Affn st 0* n in Affn & EN . (len EN) = 0* n holds
( rng (EN | ((card Affn) -' 1)) = Affn \ {(0* n)} & ( for A being Subset of (n -VectSp_over F_Real) st Affn = A holds
EN | ((card Affn) -' 1) is OrdBasis of Lin A ) )
let EN be Enumeration of Affn; :: thesis: ( 0* n in Affn & EN . (len EN) = 0* n implies ( rng (EN | ((card Affn) -' 1)) = Affn \ {(0* n)} & ( for A being Subset of (n -VectSp_over F_Real) st Affn = A holds
EN | ((card Affn) -' 1) is OrdBasis of Lin A ) ) )
set A = Affn;
set E = EN;
assume that
A1: 0* n in Affn and
A2: EN . (len EN) = 0* n ; :: thesis: ( rng (EN | ((card Affn) -' 1)) = Affn \ {(0* n)} & ( for A being Subset of (n -VectSp_over F_Real) st Affn = A holds
EN | ((card Affn) -' 1) is OrdBasis of Lin A ) )
A3: card Affn >= 1 by A1, NAT_1:14;
set cA = (card Affn) -' 1;
A4: rng EN = Affn by Def1;
(card Affn) -' 1 = (card Affn) - 1 by A1, NAT_1:14, XREAL_1:233;
then A5: len EN = ((card Affn) -' 1) + 1 by A4, FINSEQ_4:62;
A6: len EN = card Affn by A4, FINSEQ_4:62;
A7: not 0* n in rng (EN | ((card Affn) -' 1))

proof

A8: len EN in dom EN by A6, A3, FINSEQ_3:25;
assume 0* n in rng (EN | ((card Affn) -' 1)) ; :: thesis: contradiction
then consider x being object such that
A9: x in dom (EN | ((card Affn) -' 1)) and
A10: (EN | ((card Affn) -' 1)) . x = 0* n by FUNCT_1:def 3;
A11: x in Seg ((card Affn) -' 1) by A9, RELAT_1:57;
( x in dom EN & (EN | ((card Affn) -' 1)) . x = EN . x ) by A9, FUNCT_1:47, RELAT_1:57;
then x = ((card Affn) -' 1) + 1 by A2, A5, A10, A8, FUNCT_1:def 4;
then ((card Affn) -' 1) + 1 <= (card Affn) -' 1 by A11, FINSEQ_1:1;
hence contradiction by NAT_1:13; :: thesis: verum

end;

EN = (EN | ((card Affn) -' 1)) ^ <*(EN . (len EN))*> by A5, FINSEQ_3:55;
then A12: Affn = (rng (EN | ((card Affn) -' 1))) \/ (rng <*(EN . (len EN))*>) by A4, FINSEQ_1:31
.= (rng (EN | ((card Affn) -' 1))) \/ {(0* n)} by A2, FINSEQ_1:38 ;
hence A13: Affn \ {(0* n)} = rng (EN | ((card Affn) -' 1)) by A7, ZFMISC_1:117; :: thesis: for A being Subset of (n -VectSp_over F_Real) st Affn = A holds
EN | ((card Affn) -' 1) is OrdBasis of Lin A
let A1 be Subset of (n -VectSp_over F_Real); :: thesis: ( Affn = A1 implies EN | ((card Affn) -' 1) is OrdBasis of Lin A1 )
assume A14: Affn = A1 ; :: thesis: EN | ((card Affn) -' 1) is OrdBasis of Lin A1
A1 c= [#] (Lin A1)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A1 or x in [#] (Lin A1) )
assume x in A1 ; :: thesis: x in [#] (Lin A1)
then x in Lin A1 by VECTSP_7:8;
hence x in [#] (Lin A1) ; :: thesis: verum

end;

then reconsider e = EN as FinSequence of (Lin A1) by A4, A14, FINSEQ_1:def 4;
0* n = 0. (TOP-REAL n) by EUCLID:66;
then Affn \ {(0* n)} is linearly-independent by A1, RLAFFIN1:46;
then A1 \ {(0* n)} is linearly-independent by A14, MATRTOP2:7;
then A15: rng (e | ((card Affn) -' 1)) is linearly-independent by A14, A13, VECTSP_9:12;
[#] (Lin A1) = [#] (Lin Affn) by A14, MATRTOP2:6
.= [#] (Lin (Affn \ {(0. (TOP-REAL n))})) by Lm2
.= [#] (Lin (Affn \ {(0* n)})) by EUCLID:66
.= [#] (Lin (A1 \ {(0* n)})) by A14, MATRTOP2:6 ;
then Lin A1 = Lin (A1 \ {(0* n)}) by VECTSP_4:29
.= Lin (rng (e | ((card Affn) -' 1))) by A12, A7, A14, VECTSP_9:17, ZFMISC_1:117 ;
then ( e | ((card Affn) -' 1) is one-to-one & rng (e | ((card Affn) -' 1)) is Basis of (Lin A1) ) by A15, FUNCT_1:52, VECTSP_7:def 3;
hence EN | ((card Affn) -' 1) is OrdBasis of Lin A1 by MATRLIN:def 2; :: thesis: verum