begin
theorem Th1:
begin
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
:: deftheorem Def1 defines Rev AFINSQ_2:def 1 :
theorem Th8:
theorem
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem
:: deftheorem Def2 defines /^ AFINSQ_2:def 2 :
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem
:: deftheorem Def3 defines mid AFINSQ_2:def 3 :
theorem Th23:
theorem
theorem Th25:
theorem
theorem
theorem
:: deftheorem Def4 defines Sum AFINSQ_2:def 4 :
theorem
theorem
begin
definition
let X be
finite natural-membered 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 Th35:
theorem Th36:
theorem
theorem Th38:
theorem
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem
:: deftheorem defines SubXFinS AFINSQ_2:def 8 :
theorem Th47:
theorem