environ
vocabularies HIDDEN, NUMBERS, NAT_1, SUBSET_1, FINSEQ_2, EUCLID, VALUED_0, FINSEQ_1, FUNCT_1, RELAT_1, XBOOLE_0, TARSKI, FUNCT_2, CARD_1, ARYTM_1, ARYTM_3, REAL_1, PARTFUN1, ZFMISC_1, ORDINAL2, XXREAL_0, RLVECT_1, RLSUB_1, STRUCT_0, SUPINF_2, ALGSTR_0, REALSET1, MONOID_0, FUNCT_7, AFINSQ_1, RFINSEQ2, CLASSES1, RVSUM_1, COMPLEX1, SQUARE_1, REWRITE1, SETFAM_1, CARD_3, ORDINAL4, MATRIXR2, BINOP_2, XCMPLX_0, REAL_NS1, VALUED_1, RLVECT_2, MATRIX_7, FUNCOP_1, FUNCSDOM, RLVECT_3, FINSET_1, RLVECT_5, EUCLID_7;
notations HIDDEN, XBOOLE_0, TARSKI, RELAT_1, FUNCT_1, RVSUM_1, RELSET_1, PARTFUN1, CARD_1, FUNCT_2, FUNCT_3, ORDINAL1, CLASSES1, NUMBERS, SUBSET_1, XCMPLX_0, XREAL_0, COMPLEX1, FINSEQ_1, FINSEQ_2, VALUED_0, VALUED_1, FINSET_1, BINOP_1, STRUCT_0, ALGSTR_0, FUNCSDOM, MONOID_0, BINOP_2, RLVECT_1, EUCLID, SQUARE_1, XXREAL_0, SETFAM_1, RLSUB_1, RLVECT_2, RLVECT_3, REAL_1, NAT_1, NAT_D, MATRIXR2, ZFMISC_1, RLVECT_5, REALSET1, MATRIX_7, RFINSEQ2, FINSEQ_7, RUSUB_3, REAL_NS1, DOMAIN_1, RUSUB_4, FUNCOP_1;
definitions TARSKI, RVSUM_1, RLVECT_3, MONOID_0;
theorems EUCLID, RVSUM_1, FINSEQ_2, FINSEQ_1, RFUNCT_1, FINSEQ_3, SQUARE_1, ABSVALUE, JORDAN2C, XREAL_1, XXREAL_0, FUNCOP_1, XCMPLX_1, SUBSET_1, XBOOLE_0, XBOOLE_1, EUCLID_2, TARSKI, EUCLID_4, ORDINAL1, CARD_1, SETFAM_1, REAL_NS1, RLVECT_2, RLVECT_3, PARTFUN1, FUNCT_1, RLVECT_1, NAT_1, RLSUB_1, RELAT_1, REALSET1, FUNCT_2, MATRIXR2, BINOP_2, FINSOP_1, ZFMISC_1, FUNCT_3, FINSEQ_4, MATRPROB, MATRIX_7, RFINSEQ2, INTEGRA2, FINSEQ_7, INT_5, EUCLIDLP, RLVECT_5, RUSUB_1, RUSUB_3, RUSUB_4, RLVECT_4, VALUED_0, XREAL_0, VALUED_1, CLASSES1, RELSET_1, FUNCSDOM, EULER_1, NUMBERS;
schemes NAT_1, CLASSES1, FUNCT_2, FINSEQ_1;
registrations FUNCT_1, MONOID_0, RELSET_1, NUMBERS, XREAL_0, STRUCT_0, FINSET_1, XXREAL_0, CARD_1, NAT_1, MEMBERED, FINSEQ_2, EUCLID, VALUED_0, FUNCT_2, SUBSET_1, XBOOLE_0, REAL_NS1, FINSEQ_1, RELAT_1, ORDINAL1, SQUARE_1;
constructors HIDDEN, REAL_1, SQUARE_1, BINOP_2, MONOID_0, RLVECT_2, RLVECT_3, REAL_NS1, FUNCT_3, REALSET1, MATRIXR2, RLVECT_5, FINSOP_1, MATRIX_7, RFINSEQ2, SETWISEO, FINSEQ_7, RUSUB_3, RUSUB_4, NAT_D, CLASSES1, FUNCSDOM, RELSET_1, NUMBERS;
requirements HIDDEN, REAL, SUBSET, NUMERALS, ARITHM, BOOLE;
equalities SQUARE_1, FINSEQ_2, RVSUM_1, VALUED_1, RLVECT_1, BINOP_1, STRUCT_0, ALGSTR_0, FUNCSDOM, EUCLID, CARD_1, ORDINAL1;
expansions TARSKI, RVSUM_1, STRUCT_0, MONOID_0;
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 m, n being Nat st n < m holds
ex k being Nat st m = (n + 1) + k
Lm3:
0 in REAL
by XREAL_0:def 1;
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;
Lm4:
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
Lm5:
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 zero or not n is zero )
;
suppose
not
n is
zero
;
( RN_Base n is finite & card (RN_Base n) = n )
then reconsider n =
n as non
zero Nat ;
defpred S1[
object ,
object ]
means for
i being
Element of
NAT st
i = $1 holds
$2
= Base_FinSeq (
n,
i);
A1:
for
x being
object st
x in Seg n holds
ex
y being
object st
S1[
x,
y]
consider f being
Function such that A2:
(
dom f = Seg n & ( for
x2 being
object 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
object st
x1 in dom f &
x2 in dom f &
f . x1 = f . x2 holds
x1 = x2
proof
let x1,
x2 be
object ;
( 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, Th24;
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;