:: STIRL2_1 semantic presentation

definition

let c₁ be Nat;
redefine func { as {c₁} -> Subset of NAT ;
coherence by SUBSET_1:55;
let c₂ be Nat;
redefine func { as {c₁,c₂} -> Subset of NAT ;
coherence by SUBSET_1:56;
let c₃ be Nat;
redefine func { as {c₁,c₂,c₃} -> non empty Subset of NAT ;
coherence by SUBSET_1:57, ENUMSET1:def 1;

end;

theorem Th1: :: STIRL2_1:1

for b₁ being non empty Subset of NAT holds min b₁ = min* b₁

proof end;

theorem Th2: :: STIRL2_1:2

for b₁, b₂ being non empty Subset of NAT holds min (min b₁),(min b₂) = min (b₁ \/ b₂)

proof end;

theorem Th3: :: STIRL2_1:3

for b₁, b₂ being Subset of NAT holds min (min* b₁),(min* b₂) <= min* (b₁ \/ b₂)

proof end;

theorem Th4: :: STIRL2_1:4

for b₁, b₂ being Subset of NAT st not min* b₁ in b₁ /\ b₂ holds
min* b₁ = min* (b₁ \ b₂)

proof end;

theorem Th5: :: STIRL2_1:5

for b₁ being Nat holds
( min* {b₁} = b₁ & min {b₁} = b₁ )

proof end;

theorem Th6: :: STIRL2_1:6

for b₁, b₂ being Nat holds
( min* {b₁,b₂} = min b₁,b₂ & min {b₁,b₂} = min b₁,b₂ )

proof end;

theorem Th7: :: STIRL2_1:7

for b₁, b₂, b₃ being Nat holds min* {b₁,b₂,b₃} = min b₁,(min b₂,b₃)

proof end;

theorem Th8: :: STIRL2_1:8

for b₁ being Nat holds b₁ is Subset of NAT

proof end;

registration

let c₁ be Nat;
cluster -> natural Element of a₁;
coherence

proof end;

end;

theorem Th9: :: STIRL2_1:9

for b₁ being Nat
for b₂ being non empty Subset of NAT st b₂ c= b₁ holds
b₁ - 1 is Nat

proof end;

theorem Th10: :: STIRL2_1:10

for b₁, b₂ being Nat st b₁ in b₂ holds
( b₁ <= b₂ - 1 & b₂ - 1 is Nat )

proof end;

theorem Th11: :: STIRL2_1:11

for b₁ being Nat holds min* b₁ = 0

proof end;

theorem Th12: :: STIRL2_1:12

for b₁ being Nat
for b₂ being non empty Subset of NAT st b₂ c= b₁ holds
min* b₂ <= b₁ - 1

proof end;

theorem Th13: :: STIRL2_1:13

for b₁ being Nat
for b₂ being non empty Subset of NAT st b₂ c= b₁ & b₂ <> {(b₁ - 1)} holds
min* b₂ < b₁ - 1

proof end;

theorem Th14: :: STIRL2_1:14

for b₁ being Nat
for b₂ being Subset of NAT st b₂ c= b₁ & b₁ > 0 holds
min* b₂ <= b₁ - 1

proof end;

definition

let c₁ be Nat;
let c₂ be set ;
let c₃ be Function of c₁,c₂;
let c₄ be set ;
redefine func " as c₃ " c₄ -> Subset of NAT ;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be Nat;
let c₃ be Function of c₁,c₂;
let c₄ be set ;
redefine func . as c₃ . c₄ -> Element of a₂;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be Subset of NAT ;
let c₃ be Function of c₁,c₂;
let c₄ be set ;
cluster a₃ . a₄ -> natural ;
coherence

proof end;

end;

definition

let c₁, c₂ be Nat;
let c₃ be Function of c₁,c₂;
attr a₃ is "increasing means :Def1: :: STIRL2_1:def 1
( ( a₁ = 0 implies a₂ = 0 ) & ( a₂ = 0 implies a₁ = 0 ) & ( for b₁, b₂ being Nat st b₁ in rng a₃ & b₂ in rng a₃ & b₁ < b₂ holds
min* (a₃ " {b₁}) < min* (a₃ " {b₂}) ) );

end;

:: deftheorem Def1 defines "increasing STIRL2_1:def 1 :

theorem Th15: :: STIRL2_1:15

for b₁, b₂ being Nat
for b₃ being Function of b₁,b₂ st b₁ = 0 & b₂ = 0 holds
( b₃ is onto & b₃ is "increasing )

proof end;

theorem Th16: :: STIRL2_1:16

for b₁, b₂, b₃ being Nat
for b₄ being Function of b₂,b₁ st b₂ > 0 holds
min* (b₄ " {b₃}) <= b₂ - 1

proof end;

theorem Th17: :: STIRL2_1:17

for b₁, b₂ being Nat
for b₃ being Function of b₁,b₂ st b₃ is onto holds
b₁ >= b₂

proof end;

theorem Th18: :: STIRL2_1:18

for b₁, b₂ being Nat
for b₃ being Function of b₁,b₂ st b₃ is onto & b₃ is "increasing holds
for b₄ being Nat st b₄ < b₂ holds
b₄ <= min* (b₃ " {b₄})

proof end;

theorem Th19: :: STIRL2_1:19

for b₁, b₂ being Nat
for b₃ being Function of b₂,b₁ st b₃ is onto & b₃ is "increasing holds
for b₄ being Nat st b₄ < b₁ holds
min* (b₃ " {b₄}) <= (b₂ - b₁) + b₄

proof end;

theorem Th20: :: STIRL2_1:20

for b₁, b₂ being Nat
for b₃ being Function of b₁,b₂ st b₃ is onto & b₃ is "increasing & b₁ = b₂ holds
b₃ = id b₁

proof end;

theorem Th21: :: STIRL2_1:21

for b₁, b₂ being Nat
for b₃ being Function of b₂,b₁ st b₃ = id b₂ & b₂ > 0 holds
b₃ is "increasing

proof end;

theorem Th22: :: STIRL2_1:22

for b₁, b₂ being Nat holds
not ( ( b₁ = 0 implies b₂ = 0 ) & ( b₂ = 0 implies b₁ = 0 ) & ( for b₃ being Function of b₁,b₂ holds not b₃ is "increasing ) )

proof end;

theorem Th23: :: STIRL2_1:23

for b₁, b₂ being Nat holds
not ( ( b₁ = 0 implies b₂ = 0 ) & ( b₂ = 0 implies b₁ = 0 ) & b₁ >= b₂ & ( for b₃ being Function of b₁,b₂ holds
( not b₃ is onto or not b₃ is "increasing ) ) )

proof end;

scheme :: STIRL2_1:sch 1
s1{ F₁() -> Nat, F₂() -> Nat, P₁[ set ] } :

{ b₁ where B is Function of F₁(),F₂() : P₁[b₁] } is finite

proof end;

theorem Th24: :: STIRL2_1:24

for b₁, b₂ being Nat holds { b₃ where B is Function of b₁,b₂ : ( b₃ is onto & b₃ is "increasing ) } is finite

proof end;

theorem Th25: :: STIRL2_1:25

for b₁, b₂ being Nat holds Card { b₃ where B is Function of b₁,b₂ : ( b₃ is onto & b₃ is "increasing ) } is Nat

proof end;

definition

let c₁, c₂ be Nat;
func c₁ block c₂ -> Nat equals :: STIRL2_1:def 2
Card { b₁ where B is Function of a₁,a₂ : ( b₁ is onto & b₁ is "increasing ) } ;
coherence by Th25;

end;

:: deftheorem Def2 defines block STIRL2_1:def 2 :

theorem Th26: :: STIRL2_1:26

for b₁ being Nat holds b₁ block b₁ = one

proof end;

theorem Th27: :: STIRL2_1:27

for b₁ being Nat st b₁ <> 0 holds
0 block b₁ = 0

proof end;

theorem Th28: :: STIRL2_1:28

for b₁ being Nat holds
( 0 block b₁ = one iff b₁ = 0 ) by Th26, Th27;

theorem Th29: :: STIRL2_1:29

for b₁, b₂ being Nat st b₁ < b₂ holds
b₁ block b₂ = 0

proof end;

theorem Th30: :: STIRL2_1:30

for b₁ being Nat holds
( b₁ block 0 = one iff b₁ = 0 )

proof end;

theorem Th31: :: STIRL2_1:31

for b₁ being Nat st b₁ <> 0 holds
b₁ block 0 = 0

proof end;

theorem Th32: :: STIRL2_1:32

for b₁ being Nat st b₁ <> 0 holds
b₁ block 1 = one

proof end;

Lemma24: for b₁ being set holds
( Card b₁ = 0 iff b₁ is empty )
by CARD_2:59, CARD_1:47;

theorem Th33: :: STIRL2_1:33

for b₁, b₂ being Nat holds
( ( ( 1 <= b₁ & b₁ <= b₂ ) or b₁ = b₂ ) iff b₂ block b₁ > 0 )

proof end;

scheme :: STIRL2_1:sch 2
s2{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> set , F₅() -> Function of F₁(),F₂(), F₆( set ) -> set } :

ex b₁ being Function of F₃(),F₄() st
( b₁ | F₁() = F₅() & ( for b₂ being set st b₂ in F₃() \ F₁() holds
b₁ . b₂ = F₆(b₂) ) )

provided

E25: for b₁ being set st b₁ in F₃() \ F₁() holds
F₆(b₁) in F₄() and
E26: ( F₁() c= F₃() & F₂() c= F₄() ) and
E27: ( F₂() is empty implies F₁() is empty )

proof end;

scheme :: STIRL2_1:sch 3
s3{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> set , F₅( set ) -> set , P₁[ set , set , set ] } :

Card { b₁ where B is Function of F₁(),F₂() : P₁[b₁,F₁(),F₂()] } = Card { b₁ where B is Function of F₃(),F₄() : ( P₁[b₁,F₃(),F₄()] & rng (b₁ | F₁()) c= F₂() & ( for b₁ being set st b₂ in F₃() \ F₁() holds
b₁ . b₂ = F₅(b₂) ) ) }

provided

E25: for b₁ being set st b₁ in F₃() \ F₁() holds
F₅(b₁) in F₄() and
E26: ( F₁() c= F₃() & F₂() c= F₄() ) and
E27: ( F₂() is empty implies F₁() is empty ) and
E28: for b₁ being Function of F₃(),F₄() st ( for b₂ being set st b₂ in F₃() \ F₁() holds
F₅(b₂) = b₁ . b₂ ) holds
( P₁[b₁,F₃(),F₄()] iff P₁[b₁ | F₁(),F₁(),F₂()] )

proof end;

scheme :: STIRL2_1:sch 4
s4{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> set , P₁[ set , set , set ] } :

Card { b₁ where B is Function of F₁(),F₂() : P₁[b₁,F₁(),F₂()] } = Card { b₁ where B is Function of F₁() \/ {F₃()},F₂() \/ {F₄()} : ( P₁[b₁,F₁() \/ {F₃()},F₂() \/ {F₄()}] & rng (b₁ | F₁()) c= F₂() & b₁ . F₃() = F₄() ) }

provided

E25: ( F₂() is empty implies F₁() is empty ) and
E26: not F₃() in F₁() and
E27: for b₁ being Function of F₁() \/ {F₃()},F₂() \/ {F₄()} st b₁ . F₃() = F₄() holds
( P₁[b₁,F₁() \/ {F₃()},F₂() \/ {F₄()}] iff P₁[b₁ | F₁(),F₁(),F₂()] )

proof end;

theorem Th34: :: STIRL2_1:34

for b₁, b₂ being Nat
for b₃ being Function of b₁ + 1,b₂ + 1 st b₃ is onto & b₃ is "increasing & b₃ " {(b₃ . b₁)} = {b₁} holds
b₃ . b₁ = b₂

proof end;

theorem Th35: :: STIRL2_1:35

for b₁, b₂ being Nat
for b₃ being Function of b₁ + 1,b₂ st b₂ <> 0 & b₃ " {(b₃ . b₁)} <> {b₁} holds
ex b₄ being Nat st
( b₄ in b₃ " {(b₃ . b₁)} & b₄ <> b₁ )

proof end;

theorem Th36: :: STIRL2_1:36

for b₁, b₂, b₃, b₄ being Nat
for b₅ being Function of b₁,b₂
for b₆ being Function of b₁ + b₃,b₂ + b₄ st b₆ is "increasing & b₅ = b₆ | b₁ holds
for b₇, b₈ being Nat st b₇ in rng b₅ & b₈ in rng b₅ & b₇ < b₈ holds
min* (b₅ " {b₇}) < min* (b₅ " {b₈})

proof end;

theorem Th37: :: STIRL2_1:37

for b₁, b₂ being Nat
for b₃ being Function of b₁ + 1,b₂ + 1 st b₃ is onto & b₃ is "increasing & b₃ " {(b₃ . b₁)} = {b₁} holds
( rng (b₃ | b₁) c= b₂ & ( for b₄ being Function of b₁,b₂ st b₄ = b₃ | b₁ holds
( b₄ is onto & b₄ is "increasing ) ) )

proof end;

theorem Th38: :: STIRL2_1:38

for b₁, b₂ being Nat
for b₃ being Function of b₁ + 1,b₂
for b₄ being Function of b₁,b₂ st b₃ is onto & b₃ is "increasing & b₃ " {(b₃ . b₁)} <> {b₁} & b₃ | b₁ = b₄ holds
( b₄ is onto & b₄ is "increasing )

proof end;

theorem Th39: :: STIRL2_1:39

for b₁, b₂, b₃ being Nat
for b₄ being Function of b₁,b₂
for b₅ being Function of b₁ + 1,b₂ + b₃ st b₄ is onto & b₄ is "increasing & b₄ = b₅ | b₁ holds
for b₆, b₇ being Nat st b₆ in rng b₅ & b₇ in rng b₅ & b₆ < b₇ holds
min* (b₅ " {b₆}) < min* (b₅ " {b₇})

proof end;

theorem Th40: :: STIRL2_1:40

for b₁, b₂ being Nat
for b₃ being Function of b₁,b₂
for b₄ being Function of b₁ + 1,b₂ + 1 st b₃ is onto & b₃ is "increasing & b₃ = b₄ | b₁ & b₄ . b₁ = b₂ holds
( b₄ is onto & b₄ is "increasing & b₄ " {(b₄ . b₁)} = {b₁} )

proof end;

theorem Th41: :: STIRL2_1:41

for b₁, b₂ being Nat
for b₃ being Function of b₁,b₂
for b₄ being Function of b₁ + 1,b₂ st b₃ is onto & b₃ is "increasing & b₃ = b₄ | b₁ & b₄ . b₁ < b₂ holds
( b₄ is onto & b₄ is "increasing & b₄ " {(b₄ . b₁)} <> {b₁} )

proof end;

Lemma33: for b₁ being Nat holds b₁ + 1 = b₁ \/ {b₁}
by AFINSQ_1:4;

Lemma34: for b₁, b₂ being Nat st b₁ < b₂ holds
b₂ \/ {b₁} = b₂

proof end;

theorem Th42: :: STIRL2_1:42

for b₁, b₂ being Nat holds Card { b₃ where B is Function of b₁ + 1,b₂ + 1 : ( b₃ is onto & b₃ is "increasing & b₃ " {(b₃ . b₁)} = {b₁} ) } = Card { b₃ where B is Function of b₁,b₂ : ( b₃ is onto & b₃ is "increasing ) }

proof end;

theorem Th43: :: STIRL2_1:43

for b₁, b₂, b₃ being Nat st b₃ < b₁ holds
Card { b₄ where B is Function of b₂ + 1,b₁ : ( b₄ is onto & b₄ is "increasing & b₄ " {(b₄ . b₂)} <> {b₂} & b₄ . b₂ = b₃ ) } = Card { b₄ where B is Function of b₂,b₁ : ( b₄ is onto & b₄ is "increasing ) }

proof end;

definition

let c₁ be non empty set ;
let c₂ be XFinSequence of c₁;
let c₃ be BinOp of c₁;
assume E37: ( c₃ has_a_unity or len c₂ >= 1 ) ;
func c₃ "**" c₂ -> Element of a₁ means :Def3: :: STIRL2_1:def 3
a₄ = the_unity_wrt a₃ if ( a₃ has_a_unity & len a₂ = 0 )
otherwise ex b₁ being Function of NAT ,a₁ st
( b₁ . 0 = a₂ . 0 & ( for b₂ being Nat st b₂ + 1 < len a₂ holds
b₁ . (b₂ + 1) = a₃ . (b₁ . b₂),(a₂ . (b₂ + 1)) ) & a₄ = b₁ . ((len a₂) - 1) );
existence

proof end;

uniqueness

proof end;

consistency ;

end;

:: deftheorem Def3 defines "**" STIRL2_1:def 3 :

theorem Th44: :: STIRL2_1:44

for b₁ being non empty set
for b₂ being BinOp of b₁
for b₃ being Element of b₁ holds b₂ "**" <%b₃%> = b₃

proof end;

theorem Th45: :: STIRL2_1:45

for b₁ being non empty set
for b₂ being XFinSequence of b₁
for b₃ being BinOp of b₁
for b₄ being Element of b₁ st ( b₃ has_a_unity or len b₂ > 0 ) holds
b₃ "**" (b₂ ^ <%b₄%>) = b₃ . (b₃ "**" b₂),b₄

proof end;

theorem Th46: :: STIRL2_1:46

for b₁ being non empty set
for b₂ being XFinSequence of b₁ st b₂ <> <%> b₁ holds
ex b₃ being XFinSequence of b₁ex b₄ being Element of b₁ st b₂ = b₃ ^ <%b₄%>

proof end;

scheme :: STIRL2_1:sch 5
s5{ F₁() -> non empty set , P₁[ set ] } :

for b₁ being XFinSequence of F₁() holds P₁[b₁]

provided

E41: P₁[ <%> F₁()] and
E42: for b₁ being XFinSequence of F₁()
for b₂ being Element of F₁() st P₁[b₁] holds
P₁[b₁ ^ <%b₂%>]

proof end;

theorem Th47: :: STIRL2_1:47

for b₁ being non empty set
for b₂, b₃ being XFinSequence of b₁
for b₄ being BinOp of b₁ st b₄ is associative & ( b₄ has_a_unity or ( len b₂ >= 1 & len b₃ >= 1 ) ) holds
b₄ "**" (b₂ ^ b₃) = b₄ . (b₄ "**" b₂),(b₄ "**" b₃)

proof end;

definition

let c₁ be non empty set ;
let c₂, c₃ be Element of c₁;
redefine func <% as <%c₂,c₃%> -> XFinSequence of a₁;
coherence

proof end;

let c₄ be Element of c₁;
redefine func <% as <%c₂,c₃,c₄%> -> XFinSequence of a₁;
coherence

proof end;

end;

theorem Th48: :: STIRL2_1:48

for b₁ being non empty set
for b₂ being BinOp of b₁
for b₃, b₄ being Element of b₁ holds b₂ "**" <%b₃,b₄%> = b₂ . b₃,b₄

proof end;

theorem Th49: :: STIRL2_1:49

for b₁ being non empty set
for b₂ being BinOp of b₁
for b₃, b₄, b₅ being Element of b₁ holds b₂ "**" <%b₃,b₄,b₅%> = b₂ . (b₂ . b₃,b₄),b₅

proof end;

definition

let c₁ be XFinSequence of NAT ;
func Sum c₁ -> Nat equals :: STIRL2_1:def 4
addnat "**" a₁;
coherence ;

end;

:: deftheorem Def4 defines Sum STIRL2_1:def 4 :

definition

let c₁ be XFinSequence of NAT ;
let c₂ be set ;
redefine func . as c₁ . c₂ -> Nat;
coherence

proof end;

end;

theorem Th50: :: STIRL2_1:50

for b₁ being Nat
for b₂ being XFinSequence of NAT st ( for b₃ being Nat st b₃ in dom b₂ holds
b₂ . b₃ <= b₁ ) holds
Sum b₂ <= (len b₂) * b₁

proof end;

theorem Th51: :: STIRL2_1:51

for b₁ being Nat
for b₂ being XFinSequence of NAT st ( for b₃ being Nat st b₃ in dom b₂ holds
b₂ . b₃ >= b₁ ) holds
Sum b₂ >= (len b₂) * b₁

proof end;

theorem Th52: :: STIRL2_1:52

for b₁ being Nat
for b₂ being XFinSequence of NAT st len b₂ > 0 & ex b₃ being set st
( b₃ in dom b₂ & b₂ . b₃ = b₁ ) holds
Sum b₂ >= b₁

proof end;

theorem Th53: :: STIRL2_1:53

for b₁ being XFinSequence of NAT holds
( Sum b₁ = 0 iff ( len b₁ = 0 or for b₂ being Nat st b₂ in dom b₁ holds
b₁ . b₂ = 0 ) )

proof end;

theorem Th54: :: STIRL2_1:54

for b₁ being Function
for b₂ being Nat holds (union (rng (b₁ | b₂))) \/ (b₁ . b₂) = union (rng (b₁ | (b₂ + 1)))

proof end;

scheme :: STIRL2_1:sch 6
s6{ F₁() -> non empty set , F₂() -> Nat, P₁[ set , set ] } :

ex b₁ being XFinSequence of F₁() st
( dom b₁ = F₂() & ( for b₂ being Nat st b₂ in F₂() holds
P₁[b₂,b₁ . b₂] ) )

provided

E45: for b₁ being Nat st b₁ in F₂() holds
ex b₂ being Element of F₁() st P₁[b₁,b₂]

proof end;

scheme :: STIRL2_1:sch 7
s7{ F₁() -> non empty set , F₂() -> XFinSequence of F₁() } :

ex b₁ being XFinSequence of NAT st
( dom b₁ = dom F₂() & ( for b₂ being Nat st b₂ in dom b₁ holds
b₁ . b₂ = Card (F₂() . b₂) ) & Card (union (rng F₂())) = Sum b₁ )

provided

E45: for b₁ being Nat st b₁ in dom F₂() holds
F₂() . b₁ is finite and
E46: for b₁, b₂ being Nat st b₁ in dom F₂() & b₂ in dom F₂() & b₁ <> b₂ holds
F₂() . b₁ misses F₂() . b₂

proof end;

scheme :: STIRL2_1:sch 8
s8{ F₁() -> finite set , F₂() -> finite set , F₃() -> set , P₁[ set ], F₄() -> Function of card F₂(),F₂() } :

ex b₁ being XFinSequence of NAT st
( dom b₁ = card F₂() & Card { b₂ where B is Function of F₁(),F₂() : P₁[b₂] } = Sum b₁ & ( for b₂ being Nat st b₂ in dom b₁ holds
b₁ . b₂ = Card { b₃ where B is Function of F₁(),F₂() : ( P₁[b₃] & b₃ . F₃() = F₄() . b₂ ) } ) )

provided

E45: ( F₄() is onto & F₄() is one-to-one ) and
E46: not F₂() is empty and
E47: F₃() in F₁()

proof end;

theorem Th55: :: STIRL2_1:55

for b₁, b₂ being Nat holds b₁ * (b₂ block b₁) = Card { b₃ where B is Function of b₂ + 1,b₁ : ( b₃ is onto & b₃ is "increasing & b₃ " {(b₃ . b₂)} <> {b₂} ) }

proof end;

theorem Th56: :: STIRL2_1:56

for b₁, b₂ being Nat holds (b₁ + 1) block (b₂ + 1) = ((b₂ + 1) * (b₁ block (b₂ + 1))) + (b₁ block b₂)

proof end;

theorem Th57: :: STIRL2_1:57

for b₁ being Nat st b₁ >= 1 holds
b₁ block 2 = (1 / 2) * ((2 |^ b₁) - 2)

proof end;

theorem Th58: :: STIRL2_1:58

for b₁ being Nat st b₁ >= 2 holds
b₁ block 3 = (1 / 6) * (((3 |^ b₁) - (3 * (2 |^ b₁))) + 3)

proof end;

Lemma49: for b₁ being Nat holds b₁ |^ 3 = (b₁ * b₁) * b₁

proof end;

theorem Th59: :: STIRL2_1:59

for b₁ being Nat st b₁ >= 3 holds
b₁ block 4 = (1 / 24) * ((((4 |^ b₁) - (4 * (3 |^ b₁))) + (6 * (2 |^ b₁))) - 4)

proof end;

theorem Th60: :: STIRL2_1:60

( 3 ! = 6 & 4 ! = 24 )

proof end;

theorem Th61: :: STIRL2_1:61

for b₁ being Nat holds
( b₁ choose 1 = b₁ & b₁ choose 2 = (b₁ * (b₁ - 1)) / 2 & b₁ choose 3 = ((b₁ * (b₁ - 1)) * (b₁ - 2)) / 6 & b₁ choose 4 = (((b₁ * (b₁ - 1)) * (b₁ - 2)) * (b₁ - 3)) / 24 )

proof end;

theorem Th62: :: STIRL2_1:62

for b₁ being Nat holds (b₁ + 1) block b₁ = (b₁ + 1) choose 2

proof end;

theorem Th63: :: STIRL2_1:63

for b₁ being Nat holds (b₁ + 2) block b₁ = (3 * ((b₁ + 2) choose 4)) + ((b₁ + 2) choose 3)

proof end;

theorem Th64: :: STIRL2_1:64

for b₁ being Function
for b₂ being set holds
( rng (b₁ | ((dom b₁) \ (b₁ " {b₂}))) = (rng b₁) \ {b₂} & ( for b₃ being set st b₃ <> b₂ holds
(b₁ | ((dom b₁) \ (b₁ " {b₂}))) " {b₃} = b₁ " {b₃} ) )

proof end;

theorem Th65: :: STIRL2_1:65

for b₁ being Nat
for b₂, b₃ being set st Card b₂ = b₁ + 1 & b₃ in b₂ holds
Card (b₂ \ {b₃}) = b₁

proof end;

scheme :: STIRL2_1:sch 9
s9{ P₁[ set ], P₂[ set , Function] } :

for b₁ being Function st rng b₁ is finite holds
P₁[b₁]

provided

E55: P₁[ {} ] and
E56: for b₁ being Function st ( for b₂ being set st b₂ in rng b₁ & P₂[b₂,b₁] holds
P₁[b₁ | ((dom b₁) \ (b₁ " {b₂}))] ) holds
P₁[b₁]

proof end;

theorem Th66: :: STIRL2_1:66

for b₁ being Subset of NAT st b₁ is finite holds
ex b₂ being Nat st
for b₃ being Nat st b₃ in b₁ holds
b₃ <= b₂

proof end;

theorem Th67: :: STIRL2_1:67

for b₁, b₂, b₃, b₄ being set st ( b₂ is empty implies b₁ is empty ) & not b₃ in b₁ holds
for b₅ being Function of b₁,b₂ ex b₆ being Function of b₁ \/ {b₃},b₂ \/ {b₄} st
( b₆ | b₁ = b₅ & b₆ . b₃ = b₄ )

proof end;

theorem Th68: :: STIRL2_1:68

for b₁, b₂, b₃, b₄ being set st ( b₂ is empty implies b₁ is empty ) holds
for b₅ being Function of b₁,b₂
for b₆ being Function of b₁ \/ {b₃},b₂ \/ {b₄} st b₆ | b₁ = b₅ & b₆ . b₃ = b₄ holds
( ( b₅ is onto implies b₆ is onto ) & ( not b₄ in b₂ & b₅ is one-to-one implies b₆ is one-to-one ) )

proof end;

Lemma58: for b₁, b₂ being set st b₂ in b₁ holds
(b₁ \ {b₂}) \/ {b₂} = b₁
by ZFMISC_1:140;

theorem Th69: :: STIRL2_1:69

for b₁ being finite Subset of NAT ex b₂ being Function of b₁, card b₁ st
( b₂ is bijective & ( for b₃, b₄ being Nat st b₃ in dom b₂ & b₄ in dom b₂ & b₃ < b₄ holds
b₂ . b₃ < b₂ . b₄ ) )

proof end;

Lemma60: for b₁ being finite set
for b₂ being set st b₂ in b₁ holds
card (b₁ \ {b₂}) < card b₁

proof end;

theorem Th70: :: STIRL2_1:70

for b₁, b₂ being finite set
for b₃ being Function of b₁,b₂ st card b₁ = card b₂ holds
( b₃ is onto iff b₃ is one-to-one )

proof end;

Lemma62: for b₁ being Nat
for b₂ being finite Subset of NAT
for b₃ being Function of b₂, card b₂ st b₁ in b₂ & b₃ is bijective & ( for b₄, b₅ being Nat st b₄ in dom b₃ & b₅ in dom b₃ & b₄ < b₅ holds
b₃ . b₄ < b₃ . b₅ ) holds
ex b₄ being Permutation of b₂ st
for b₅ being Nat st b₅ in b₂ holds
( ( b₅ < b₁ implies b₄ . b₅ = (b₃ " ) . ((b₃ . b₅) + 1) ) & ( b₅ = b₁ implies b₄ . b₅ = (b₃ " ) . 0 ) & ( b₅ > b₁ implies b₄ . b₅ = b₅ ) )

proof end;

theorem Th71: :: STIRL2_1:71

for b₁, b₂ being Function
for b₃ being set st b₃ in rng (b₂ * b₁) & b₂ is one-to-one holds
ex b₄ being set st
( b₄ in dom b₂ & b₄ in rng b₁ & b₂ " {b₃} = {b₄} & b₁ " {b₄} = (b₂ * b₁) " {b₃} )

proof end;

definition

let c₁, c₂ be Subset of NAT ;
let c₃ be Function of c₁,c₂;
attr a₃ is "increasing means :Def5: :: STIRL2_1:def 5
for b₁, b₂ being Nat st b₁ in rng a₃ & b₂ in rng a₃ & b₁ < b₂ holds
min* (a₃ " {b₁}) < min* (a₃ " {b₂});

end;

:: deftheorem Def5 defines "increasing STIRL2_1:def 5 :

theorem Th72: :: STIRL2_1:72

for b₁, b₂ being Subset of NAT
for b₃ being Function of b₁,b₂ st b₃ is "increasing holds
min* (rng b₃) = b₃ . (min* (dom b₃))

proof end;

theorem Th73: :: STIRL2_1:73

for b₁, b₂ being Subset of NAT
for b₃ being Function of b₁,b₂ st rng b₃ is finite holds
ex b₄ being Function of b₁,b₂ex b₅ being Permutation of rng b₃ st
( b₃ = b₅ * b₄ & rng b₃ = rng b₄ & b₄ is "increasing )

proof end;

theorem Th74: :: STIRL2_1:74

for b₁, b₂, b₃ being Subset of NAT
for b₄ being Function of b₁,b₂ st rng b₄ is finite holds
for b₅, b₆ being Function of b₁,b₃
for b₇, b₈ being Function st b₇ is one-to-one & b₈ is one-to-one & rng b₅ = rng b₆ & rng b₅ = dom b₇ & dom b₇ = dom b₈ & b₄ = b₇ * b₅ & b₄ = b₈ * b₆ & b₅ is "increasing & b₆ is "increasing holds
( b₇ = b₈ & b₅ = b₆ )

proof end;

theorem Th75: :: STIRL2_1:75

for b₁, b₂ being Subset of NAT
for b₃ being Function of b₁,b₂ st rng b₃ is finite holds
for b₄, b₅ being Function of b₁,b₂
for b₆, b₇ being Permutation of rng b₃ st b₃ = b₆ * b₄ & b₃ = b₇ * b₅ & rng b₃ = rng b₄ & rng b₃ = rng b₅ & b₄ is "increasing & b₅ is "increasing holds
( b₆ = b₇ & b₄ = b₅ )

proof end;