begin
Lm1:
for X being set
for Y being non empty set
for f being Function of X,Y st f is bijective holds
card X = card Y
by EULER_1:11;
Lm2:
for n, m being Nat st n < m holds
ex k being Nat st m = (n + 1) + k
begin
begin
begin
definition
let n be
Nat;
let x0 be
Element of
REAL n;
existence
ex b1 being FinSequence of REAL n st
( len b1 = n & ( for i being Nat st 1 <= i & i <= n holds
b1 . i = |(x0,(Base_FinSeq (n,i)))| * (Base_FinSeq (n,i)) ) )
uniqueness
for b1, b2 being FinSequence of REAL n st len b1 = n & ( for i being Nat st 1 <= i & i <= n holds
b1 . i = |(x0,(Base_FinSeq (n,i)))| * (Base_FinSeq (n,i)) ) & len b2 = n & ( for i being Nat st 1 <= i & i <= n holds
b2 . i = |(x0,(Base_FinSeq (n,i)))| * (Base_FinSeq (n,i)) ) holds
b1 = b2
end;
begin
Lm3:
for n being Nat
for X being Subspace of RealVectSpace (Seg n)
for x, y being Element of REAL n
for a being Real st x in the carrier of X & y in the carrier of X holds
(a * x) + y in the carrier of X
Lm4:
now for n being Nat holds
( RN_Base n is finite & card (RN_Base n) = n )
let n be
Nat;
( RN_Base n is finite & card (RN_Base n) = n )thus
(
RN_Base n is
finite &
card (RN_Base n) = n )
verum
proof
per cases
( n is empty or not n is empty )
;
suppose
not
n is
empty
;
( RN_Base n is finite & card (RN_Base n) = n )
then reconsider n =
n as non
empty Nat ;
defpred S1[
set ,
set ]
means for
i being
Element of
NAT st
i = $1 holds
$2
= Base_FinSeq (
n,
i);
A1:
for
x being
set st
x in Seg n holds
ex
y being
set st
S1[
x,
y]
consider f being
Function such that A2:
(
dom f = Seg n & ( for
x2 being
set st
x2 in Seg n holds
S1[
x2,
f . x2] ) )
from CLASSES1:sch 1(A1);
A3:
rng f c= RN_Base n
then reconsider f2 =
f as
Function of
(Seg n),
(RN_Base n) by A2, FUNCT_2:2;
for
x1,
x2 being
set st
x1 in dom f &
x2 in dom f &
f . x1 = f . x2 holds
x1 = x2
proof
let x1,
x2 be
set ;
( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that A8:
x1 in dom f
and A9:
x2 in dom f
and A10:
f . x1 = f . x2
;
x1 = x2
reconsider nx1 =
x1,
nx2 =
x2 as
Element of
NAT by A2, A8, A9;
A11:
nx1 <= n
by A2, A8, FINSEQ_1:1;
A12:
f . x2 = Base_FinSeq (
n,
nx2)
by A2, A9;
A13:
f . x1 = Base_FinSeq (
n,
nx1)
by A2, A8;
1
<= nx1
by A2, A8, FINSEQ_1:1;
hence
x1 = x2
by A10, A11, A13, A12, Th25;
verum
end;
then A14:
f2 is
one-to-one
by FUNCT_1:def 4;
RN_Base n c= rng f
then
rng f = RN_Base n
by A3, XBOOLE_0:def 10;
then
f2 is
onto
by FUNCT_2:def 3;
then
card (Seg n) = card (RN_Base n)
by A14, Lm1;
hence
(
RN_Base n is
finite &
card (RN_Base n) = n )
by FINSEQ_1:57;
verum
end;
end;
end;
end;
begin