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 )
theorem Th1:
begin
theorem Th2:
theorem Th3:
theorem Th4:
theorem
canceled;
theorem
canceled;
theorem
canceled;
:: deftheorem Def1 defines Rev AFINSQ_2:def 1 :
theorem Th8:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
Th9:
for p being XFinSequence st p <> {} holds
ex q being XFinSequence ex x being set st p = q ^ <%x%>
by AFINSQ_1:44;
Th10:
for n being Nat
for p being XFinSequence st len p <= n holds
p | n = p
by AFINSQ_1:56;
Th11:
for n, m being Nat
for p being XFinSequence st n <= len p & m in n holds
( (p | n) . m = p . m & m in dom p )
by AFINSQ_1:57;
Th12:
for i being Nat
for p being XFinSequence st i <= len p holds
len (p | i) = i
by AFINSQ_1:58;
Th13:
for i being Nat
for p being XFinSequence holds len (p | i) <= i
by AFINSQ_1:59;
:: deftheorem Def2 defines /^ AFINSQ_2:def 2 :
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem
:: deftheorem defines mid AFINSQ_2:def 3 :
theorem Th23:
theorem
theorem Th25:
theorem
theorem
theorem
definition
canceled;
end;
:: deftheorem AFINSQ_2:def 4 :
canceled;
theorem
canceled;
theorem
canceled;
begin
definition
let X be
natural-membered finite set ;
func Sgm0 X -> XFinSequence of
NAT means :
Def5:
(
rng it = X & ( for
l,
m,
k1,
k2 being
Nat st
l < m &
m < len it &
k1 = it . l &
k2 = it . m holds
k1 < k2 ) );
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;
:: deftheorem Def5 defines Sgm0 AFINSQ_2:def 5 :
theorem Th31:
theorem Th32:
theorem Th33:
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;
:: deftheorem Def6 defines <N< AFINSQ_2:def 6 :
for
B1,
B2 being
set holds
(
B1 <N< B2 iff for
n,
m being
Nat st
n in B1 &
m in B2 holds
n < m );
definition
let B1,
B2 be
set ;
pred B1 <N= B2 means :
Def7:
for
n,
m being
Nat st
n in B1 &
m in B2 holds
n <= m;
end;
:: deftheorem Def7 defines <N= AFINSQ_2:def 7 :
for
B1,
B2 being
set holds
(
B1 <N= B2 iff for
n,
m being
Nat st
n in B1 &
m in B2 holds
n <= m );
theorem Th34:
theorem
theorem Th36:
theorem
theorem Th38:
theorem
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
:: deftheorem defines SubXFinS AFINSQ_2:def 8 :
theorem Th47:
theorem
canceled;
:: deftheorem Def9 defines "**" AFINSQ_2:def 9 :
theorem Th50:
theorem Th51:
theorem
theorem Th53:
theorem
theorem Th55:
theorem Th56:
theorem Th57:
theorem Th58:
theorem
theorem Th60:
Lm6:
for cF being complex-valued XFinSequence holds cF is COMPLEX -valued
Lm7:
for rF being real-valued XFinSequence holds rF is REAL -valued
:: deftheorem defines Sum AFINSQ_2:def 10 :
theorem Th61:
theorem Th62:
theorem Th63:
theorem Th64:
theorem TH:
theorem
theorem
theorem Th65:
theorem
theorem Th67:
theorem Th68:
theorem
theorem
theorem Th71:
theorem Th72:
theorem TTT1:
theorem
theorem Th74:
theorem Th75:
theorem Th76:
theorem
theorem
theorem Th79:
theorem