reconsider n = n as Element of NAT by ORDINAL1:def 12;
deffunc H₁( Nat) -> Element of n -tuples_on the carrier of R = R _th_unit_vector (n,R);
defpred S₁[ Nat] means ( 1 <= R & R <= n );
D: { H₁(i) where i is Nat : ( i <= n & S₁[i] ) } is finite from FINSEQ_1:sch 6();

E: now :: thesis: for o being object st o in { H₁(i) where i is Nat : ( i <= n & S₁[i] ) } holds
o in Base (R,n)

let o be object ; :: thesis: ( o in { H₁(i) where i is Nat : ( i <= n & S₁[i] ) } implies o in Base (R,n) )
assume o in { H₁(i) where i is Nat : ( i <= n & S₁[i] ) } ; :: thesis: o in Base (R,n)
then consider i being Nat such that
F: ( o = i _th_unit_vector (n,R) & i <= n & 1 <= i & i <= n ) ;
thus o in Base (R,n) by F; :: thesis: verum

end;

now :: thesis: for o being object st o in Base (R,n) holds
o in { H₁(i) where i is Nat : ( i <= n & S₁[i] ) }

let o be object ; :: thesis: ( o in Base (R,n) implies o in { H₁(i) where i is Nat : ( i <= n & S₁[i] ) } )
assume o in Base (R,n) ; :: thesis: o in { H₁(i) where i is Nat : ( i <= n & S₁[i] ) }
then consider i being Nat such that
F: ( o = i _th_unit_vector (n,R) & 1 <= i & i <= n ) ;
thus o in { H₁(i) where i is Nat : ( i <= n & S₁[i] ) } by F; :: thesis: verum

end;

hence Base (R,n) is finite by D, E, TARSKI:2; :: thesis: verum