let R be non degenerated Ring; :: thesis: for n being Nat holds card (Base (R,n)) = n
let n be Nat; :: thesis: card (Base (R,n)) = n
defpred S₁[ object , object ] means ex x being Nat st
( $1 = x & $2 = x _th_unit_vector (n,R) );
B1: for x, y1, y2 being object st x in Seg n & S₁[x,y1] & S₁[x,y2] holds
y1 = y2 ;

B2: now :: thesis: for x being object st x in Seg n holds
ex y being object st S₁[x,y]

let x be object ; :: thesis: ( x in Seg n implies ex y being object st S₁[x,y] )
assume x in Seg n ; :: thesis: ex y being object st S₁[x,y]
then reconsider k = x as Nat ;
thus ex y being object st S₁[x,y] :: thesis: verum

proof

take k _th_unit_vector (n,R) ; :: thesis: S₁[x,k _th_unit_vector (n,R)]
thus S₁[x,k _th_unit_vector (n,R)] ; :: thesis: verum

end;

end;

consider f being Function such that
C: ( dom f = Seg n & ( for x being object st x in Seg n holds
S₁[x,f . x] ) ) from FUNCT_1:sch 2(B1, B2);

A1: now :: thesis: for o being object st o in Base (R,n) holds
o in rng f

let o be object ; :: thesis: ( o in Base (R,n) implies o in rng f )
assume o in Base (R,n) ; :: thesis: o in rng f
then consider i being Nat such that
A2: ( o = i _th_unit_vector (n,R) & 1 <= i & i <= n ) ;
A4: i in Seg n by A2;
S₁[i,f . i] by C, FINSEQ_1:1, A2;
hence o in rng f by A4, C, A2, FUNCT_1:def 3; :: thesis: verum

end;

now :: thesis: for o being object st o in rng f holds
o in Base (R,n)

let o be object ; :: thesis: ( o in rng f implies o in Base (R,n) )
assume o in rng f ; :: thesis: o in Base (R,n)
then consider u being object such that
A2: ( u in dom f & o = f . u ) by FUNCT_1:def 3;
reconsider j = u as Element of NAT by A2, C;
S₁[u,f . u] by C, A2;
then consider i being Element of Seg n such that
A3: ( u = i & f . u = j _th_unit_vector (n,R) ) by C, A2;
( 1 <= j & j <= n ) by A2, C, FINSEQ_1:1;
hence o in Base (R,n) by A2, A3; :: thesis: verum

end;

then A: rng f = Base (R,n) by A1, TARSKI:2;

now :: thesis: f is one-to-one

assume not f is one-to-one ; :: thesis: contradiction
then consider x1, x2 being object such that
A1: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 & x1 <> x2 ) ;
reconsider j1 = x1, j2 = x2 as Element of NAT by A1, C;
S₁[x1,f . x1] by C, A1;
then consider i1 being Element of Seg n such that
A2: ( i1 = x1 & f . x1 = j1 _th_unit_vector (n,R) ) by C, A1;
S₁[x2,f . x2] by C, A1;
then consider i2 being Element of Seg n such that
A3: ( i2 = x2 & f . x2 = j2 _th_unit_vector (n,R) ) by C, A1;
( 1 <= j1 & j1 <= n & 1 <= j2 & j2 <= n ) by A1, C, FINSEQ_1:1;
hence contradiction by u2, A1, A2, A3; :: thesis: verum

end;

then card (Base (R,n)) = card (Seg n) by A, C, CARD_1:70
.= n by FINSEQ_1:57 ;
hence card (Base (R,n)) = n ; :: thesis: verum