begin
Lm1:
for X, Y being finite set st X c= Y & card X = card Y holds
X = Y
Lm2:
for X, Y being finite set
for F being Function of X,Y st card X = card Y holds
( F is onto iff F is one-to-one )
begin
begin
definition
let X be
finite natural-membered set ;
existence
ex b1 being XFinSequence of NAT st
( rng b1 = X & ( for l, m, k1, k2 being Nat st l < m & m < len b1 & k1 = b1 . l & k2 = b1 . m holds
k1 < k2 ) )
uniqueness
for b1, b2 being XFinSequence of NAT st rng b1 = X & ( for l, m, k1, k2 being Nat st l < m & m < len b1 & k1 = b1 . l & k2 = b1 . m holds
k1 < k2 ) & rng b2 = X & ( for l, m, k1, k2 being Nat st l < m & m < len b2 & k1 = b2 . l & k2 = b2 . m holds
k1 < k2 ) holds
b1 = b2
end;
definition
let B1,
B2 be
set ;
pred B1 <N< B2 means :
Def5:
for
n,
m being
Nat st
n in B1 &
m in B2 holds
n < m;
end;
definition
let B1,
B2 be
set ;
pred B1 <N= B2 means :
Def6:
for
n,
m being
Nat st
n in B1 &
m in B2 holds
n <= m;
end;
Lm3:
for cF being complex-valued XFinSequence holds cF is COMPLEX -valued
Lm4:
for rF being real-valued XFinSequence holds rF is REAL -valued