let n be Nat; :: thesis: for Affn being affinely-independent Subset of ()
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 () st Affn = A holds
EN | ((card Affn) -' 1) is OrdBasis of Lin A ) )

let Affn be affinely-independent Subset of (); :: 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 () 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 () 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 () st Affn = A holds
EN | ((card Affn) -' 1) is OrdBasis of Lin A ) )

A3: card Affn >= 1 by ;
set cA = (card Affn) -' 1;
A4: rng EN = Affn by Def1;
(card Affn) -' 1 = (card Affn) - 1 by ;
then A5: len EN = ((card Affn) -' 1) + 1 by ;
A6: len EN = card Affn by ;
A7: not 0* n in rng (EN | ((card Affn) -' 1))
proof
A8: len EN in dom EN by ;
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 ;
( x in dom EN & (EN | ((card Affn) -' 1)) . x = EN . x ) by ;
then x = ((card Affn) -' 1) + 1 by ;
then ((card Affn) -' 1) + 1 <= (card Affn) -' 1 by ;
hence contradiction by NAT_1:13; :: thesis: verum
end;
EN = (EN | ((card Affn) -' 1)) ^ <*(EN . (len EN))*> by ;
then A12: Affn = (rng (EN | ((card Affn) -' 1))) \/ (rng <*(EN . (len EN))*>) by
.= (rng (EN | ((card Affn) -' 1))) \/ {(0* n)} by ;
hence A13: Affn \ {(0* n)} = rng (EN | ((card Affn) -' 1)) by ; :: thesis: for A being Subset of () st Affn = A holds
EN | ((card Affn) -' 1) is OrdBasis of Lin A

let A1 be Subset of (); :: 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 ;
0* n = 0. () by EUCLID:66;
then Affn \ {(0* n)} is linearly-independent by ;
then A1 \ {(0* n)} is linearly-independent by ;
then A15: rng (e | ((card Affn) -' 1)) is linearly-independent by ;
[#] (Lin A1) = [#] (Lin Affn) by
.= [#] (Lin (Affn \ {(0. ())})) by Lm2
.= [#] (Lin (Affn \ {(0* n)})) by EUCLID:66
.= [#] (Lin (A1 \ {(0* n)})) by ;
then Lin A1 = Lin (A1 \ {(0* n)}) by VECTSP_4:29
.= Lin (rng (e | ((card Affn) -' 1))) by ;
then ( e | ((card Affn) -' 1) is one-to-one & rng (e | ((card Affn) -' 1)) is Basis of (Lin A1) ) by ;
hence EN | ((card Affn) -' 1) is OrdBasis of Lin A1 by MATRLIN:def 2; :: thesis: verum