:: FINSEQ_4 semantic presentation

definition

let c₁ be Function;
let c₂ be set ;
pred c₁ is_one-to-one_at c₂ means :Def1: :: FINSEQ_4:def 1
a₁ " (a₁ .: {a₂}) = {a₂};

end;

:: deftheorem Def1 defines is_one-to-one_at FINSEQ_4:def 1 :

theorem Th1: :: FINSEQ_4:1

canceled;

theorem Th2: :: FINSEQ_4:2

for b₁ being Function
for b₂ being set st b₁ is_one-to-one_at b₂ holds
b₂ in dom b₁

proof end;

theorem Th3: :: FINSEQ_4:3

for b₁ being Function
for b₂ being set holds
( b₁ is_one-to-one_at b₂ iff ( b₂ in dom b₁ & b₁ " {(b₁ . b₂)} = {b₂} ) )

proof end;

theorem Th4: :: FINSEQ_4:4

for b₁ being Function
for b₂ being set holds
( b₁ is_one-to-one_at b₂ iff ( b₂ in dom b₁ & ( for b₃ being set st b₃ in dom b₁ & b₂ <> b₃ holds
b₁ . b₂ <> b₁ . b₃ ) ) )

proof end;

theorem Th5: :: FINSEQ_4:5

for b₁ being Function holds
( ( for b₂ being set st b₂ in dom b₁ holds
b₁ is_one-to-one_at b₂ ) iff b₁ is one-to-one )

proof end;

definition

let c₁ be Function;
let c₂ be set ;
pred c₁ just_once_values c₂ means :Def2: :: FINSEQ_4:def 2
ex b₁ being finite set st
( b₁ = a₁ " {a₂} & card b₁ = 1 );

end;

:: deftheorem Def2 defines just_once_values FINSEQ_4:def 2 :

theorem Th6: :: FINSEQ_4:6

canceled;

theorem Th7: :: FINSEQ_4:7

for b₁ being Function
for b₂ being set st b₁ just_once_values b₂ holds
b₂ in rng b₁

proof end;

theorem Th8: :: FINSEQ_4:8

for b₁ being Function
for b₂ being set holds
( b₁ just_once_values b₂ iff ex b₃ being set st {b₃} = b₁ " {b₂} )

proof end;

theorem Th9: :: FINSEQ_4:9

for b₁ being Function
for b₂ being set holds
( b₁ just_once_values b₂ iff ex b₃ being set st
( b₃ in dom b₁ & b₂ = b₁ . b₃ & ( for b₄ being set st b₄ in dom b₁ & b₄ <> b₃ holds
b₁ . b₄ <> b₂ ) ) )

proof end;

theorem Th10: :: FINSEQ_4:10

for b₁ being Function holds
( b₁ is one-to-one iff for b₂ being set st b₂ in rng b₁ holds
b₁ just_once_values b₂ )

proof end;

theorem Th11: :: FINSEQ_4:11

for b₁ being Function
for b₂ being set holds
( b₁ is_one-to-one_at b₂ iff ( b₂ in dom b₁ & b₁ just_once_values b₁ . b₂ ) )

proof end;

definition

let c₁ be Function;
let c₂ be set ;
assume E11: c₁ just_once_values c₂ ;
func c₁ <- c₂ -> set means :Def3: :: FINSEQ_4:def 3
( a₃ in dom a₁ & a₁ . a₃ = a₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines <- FINSEQ_4:def 3 :

theorem Th12: :: FINSEQ_4:12

canceled;

theorem Th13: :: FINSEQ_4:13

canceled;

theorem Th14: :: FINSEQ_4:14

canceled;

theorem Th15: :: FINSEQ_4:15

canceled;

theorem Th16: :: FINSEQ_4:16

for b₁ being Function
for b₂ being set st b₁ just_once_values b₂ holds
b₁ .: {(b₁ <- b₂)} = {b₂}

proof end;

theorem Th17: :: FINSEQ_4:17

for b₁ being Function
for b₂ being set st b₁ just_once_values b₂ holds
b₁ " {b₂} = {(b₁ <- b₂)}

proof end;

theorem Th18: :: FINSEQ_4:18

for b₁ being Function
for b₂ being set st b₁ is one-to-one & b₂ in rng b₁ holds
(b₁ " ) . b₂ = b₁ <- b₂

proof end;

theorem Th19: :: FINSEQ_4:19

canceled;

theorem Th20: :: FINSEQ_4:20

for b₁ being Function
for b₂ being set st b₁ is_one-to-one_at b₂ holds
b₁ <- (b₁ . b₂) = b₂

proof end;

theorem Th21: :: FINSEQ_4:21

for b₁ being Function
for b₂ being set st b₁ just_once_values b₂ holds
b₁ is_one-to-one_at b₁ <- b₂

proof end;

definition

let c₁ be non empty set ;
let c₂, c₃ be Element of c₁;
redefine func <* as <*c₂,c₃*> -> FinSequence of a₁;
coherence by FINSEQ_2:15;

end;

definition

let c₁ be non empty set ;
let c₂, c₃, c₄ be Element of c₁;
redefine func <* as <*c₂,c₃,c₄*> -> FinSequence of a₁;
coherence by FINSEQ_2:16;

end;

definition

let c₁, c₂ be set ;
let c₃ be PartFunc of c₁,c₂;
let c₄ be set ;
assume E13: c₄ in dom c₃ ;
func c₃ /. c₄ -> Element of a₂ equals :Def4: :: FINSEQ_4:def 4
a₃ . a₄;
coherence by E13, PARTFUN1:27;

end;

:: deftheorem Def4 defines /. FINSEQ_4:def 4 :

theorem Th22: :: FINSEQ_4:22

for b₁, b₂ being non empty set
for b₃ being Function of b₁,b₂
for b₄ being Element of b₁ holds b₃ /. b₄ = b₃ . b₄

proof end;

theorem Th23: :: FINSEQ_4:23

canceled;

theorem Th24: :: FINSEQ_4:24

for b₁ being set
for b₂ being FinSequence of b₁
for b₃ being Nat st 1 <= b₃ & b₃ <= len b₂ holds
b₂ /. b₃ = b₂ . b₃

proof end;

theorem Th25: :: FINSEQ_4:25

for b₁ being non empty set
for b₂ being Element of b₁ holds <*b₂*> /. 1 = b₂

proof end;

theorem Th26: :: FINSEQ_4:26

for b₁ being non empty set
for b₂, b₃ being Element of b₁ holds
( <*b₂,b₃*> /. 1 = b₂ & <*b₂,b₃*> /. 2 = b₃ )

proof end;

theorem Th27: :: FINSEQ_4:27

for b₁ being non empty set
for b₂, b₃, b₄ being Element of b₁ holds
( <*b₂,b₃,b₄*> /. 1 = b₂ & <*b₂,b₃,b₄*> /. 2 = b₃ & <*b₂,b₃,b₄*> /. 3 = b₄ )

proof end;

definition

let c₁ be FinSequence;
let c₂ be set ;
func c₂ .. c₁ -> Nat equals :: FINSEQ_4:def 5
(Sgm (a₁ " {a₂})) . 1;
coherence

proof end;

end;

:: deftheorem Def5 defines .. FINSEQ_4:def 5 :

theorem Th28: :: FINSEQ_4:28

canceled;

theorem Th29: :: FINSEQ_4:29

for b₁ being FinSequence
for b₂ being set st b₂ in rng b₁ holds
b₁ . (b₂ .. b₁) = b₂

proof end;

theorem Th30: :: FINSEQ_4:30

for b₁ being FinSequence
for b₂ being set st b₂ in rng b₁ holds
b₂ .. b₁ in dom b₁

proof end;

theorem Th31: :: FINSEQ_4:31

for b₁ being FinSequence
for b₂ being set st b₂ in rng b₁ holds
( 1 <= b₂ .. b₁ & b₂ .. b₁ <= len b₁ )

proof end;

theorem Th32: :: FINSEQ_4:32

for b₁ being FinSequence
for b₂ being set st b₂ in rng b₁ holds
( (b₂ .. b₁) - 1 is Nat & (len b₁) - (b₂ .. b₁) is Nat )

proof end;

theorem Th33: :: FINSEQ_4:33

for b₁ being FinSequence
for b₂ being set st b₂ in rng b₁ holds
b₂ .. b₁ in b₁ " {b₂}

proof end;

theorem Th34: :: FINSEQ_4:34

for b₁ being FinSequence
for b₂ being set
for b₃ being Nat st b₃ in dom b₁ & b₃ < b₂ .. b₁ holds
b₁ . b₃ <> b₂

proof end;

theorem Th35: :: FINSEQ_4:35

for b₁ being FinSequence
for b₂ being set st b₁ just_once_values b₂ holds
b₁ <- b₂ = b₂ .. b₁

proof end;

theorem Th36: :: FINSEQ_4:36

for b₁ being FinSequence
for b₂ being set st b₁ just_once_values b₂ holds
for b₃ being Nat st b₃ in dom b₁ & b₃ <> b₂ .. b₁ holds
b₁ . b₃ <> b₂

proof end;

theorem Th37: :: FINSEQ_4:37

for b₁ being FinSequence
for b₂ being set st b₂ in rng b₁ & ( for b₃ being Nat st b₃ in dom b₁ & b₃ <> b₂ .. b₁ holds
b₁ . b₃ <> b₂ ) holds
b₁ just_once_values b₂

proof end;

theorem Th38: :: FINSEQ_4:38

for b₁ being FinSequence
for b₂ being set holds
( b₁ just_once_values b₂ iff ( b₂ in rng b₁ & {(b₂ .. b₁)} = b₁ " {b₂} ) )

proof end;

theorem Th39: :: FINSEQ_4:39

for b₁ being FinSequence
for b₂ being set st b₁ is one-to-one & b₂ in rng b₁ holds
{(b₂ .. b₁)} = b₁ " {b₂}

proof end;

theorem Th40: :: FINSEQ_4:40

for b₁ being FinSequence
for b₂ being set holds
( b₁ just_once_values b₂ iff len (b₁ - {b₂}) = (len b₁) - 1 )

proof end;

theorem Th41: :: FINSEQ_4:41

for b₁ being FinSequence
for b₂ being set st b₁ just_once_values b₂ holds
for b₃ being Nat st b₃ in dom (b₁ - {b₂}) holds
( ( b₃ < b₂ .. b₁ implies (b₁ - {b₂}) . b₃ = b₁ . b₃ ) & ( b₂ .. b₁ <= b₃ implies (b₁ - {b₂}) . b₃ = b₁ . (b₃ + 1) ) )

proof end;

theorem Th42: :: FINSEQ_4:42

for b₁ being FinSequence
for b₂ being set st b₁ is one-to-one & b₂ in rng b₁ holds
for b₃ being Nat st b₃ in dom (b₁ - {b₂}) holds
( ( (b₁ - {b₂}) . b₃ = b₁ . b₃ implies b₃ < b₂ .. b₁ ) & ( b₃ < b₂ .. b₁ implies (b₁ - {b₂}) . b₃ = b₁ . b₃ ) & ( (b₁ - {b₂}) . b₃ = b₁ . (b₃ + 1) implies b₂ .. b₁ <= b₃ ) & ( b₂ .. b₁ <= b₃ implies (b₁ - {b₂}) . b₃ = b₁ . (b₃ + 1) ) )

proof end;

definition

let c₁ be FinSequence;
let c₂ be set ;
assume E26: c₂ in rng c₁ ;
func c₁ -| c₂ -> FinSequence means :Def6: :: FINSEQ_4:def 6
ex b₁ being Nat st
( b₁ = (a₂ .. a₁) - 1 & a₃ = a₁ | (Seg b₁) );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def6 defines -| FINSEQ_4:def 6 :

theorem Th43: :: FINSEQ_4:43

canceled;

theorem Th44: :: FINSEQ_4:44

canceled;

theorem Th45: :: FINSEQ_4:45

for b₁ being FinSequence
for b₂ being set
for b₃ being Nat st b₂ in rng b₁ & b₃ = (b₂ .. b₁) - 1 holds
b₁ | (Seg b₃) = b₁ -| b₂

proof end;

theorem Th46: :: FINSEQ_4:46

for b₁ being FinSequence
for b₂ being set st b₂ in rng b₁ holds
len (b₁ -| b₂) = (b₂ .. b₁) - 1

proof end;

theorem Th47: :: FINSEQ_4:47

for b₁ being FinSequence
for b₂ being set
for b₃ being Nat st b₂ in rng b₁ & b₃ = (b₂ .. b₁) - 1 holds
dom (b₁ -| b₂) = Seg b₃

proof end;

theorem Th48: :: FINSEQ_4:48

for b₁ being FinSequence
for b₂ being set
for b₃ being Nat st b₂ in rng b₁ & b₃ in dom (b₁ -| b₂) holds
b₁ . b₃ = (b₁ -| b₂) . b₃

proof end;

theorem Th49: :: FINSEQ_4:49

for b₁ being FinSequence
for b₂ being set st b₂ in rng b₁ holds
not b₂ in rng (b₁ -| b₂)

proof end;

theorem Th50: :: FINSEQ_4:50

for b₁ being FinSequence
for b₂ being set st b₂ in rng b₁ holds
rng (b₁ -| b₂) misses {b₂}

proof end;

theorem Th51: :: FINSEQ_4:51

for b₁ being FinSequence
for b₂ being set st b₂ in rng b₁ holds
rng (b₁ -| b₂) c= rng b₁

proof end;

theorem Th52: :: FINSEQ_4:52

for b₁ being FinSequence
for b₂ being set st b₂ in rng b₁ holds
( b₂ .. b₁ = 1 iff b₁ -| b₂ = {} )

proof end;

theorem Th53: :: FINSEQ_4:53

for b₁ being FinSequence
for b₂ being set
for b₃ being non empty set st b₂ in rng b₁ & b₁ is FinSequence of b₃ holds
b₁ -| b₂ is FinSequence of b₃

proof end;

definition

let c₁ be FinSequence;
let c₂ be set ;
assume E32: c₂ in rng c₁ ;
func c₁ |-- c₂ -> FinSequence means :Def7: :: FINSEQ_4:def 7
( len a₃ = (len a₁) - (a₂ .. a₁) & ( for b₁ being Nat st b₁ in dom a₃ holds
a₃ . b₁ = a₁ . (b₁ + (a₂ .. a₁)) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines |-- FINSEQ_4:def 7 :

theorem Th54: :: FINSEQ_4:54

canceled;

theorem Th55: :: FINSEQ_4:55

canceled;

theorem Th56: :: FINSEQ_4:56

canceled;

theorem Th57: :: FINSEQ_4:57

for b₁ being FinSequence
for b₂ being set
for b₃ being Nat st b₂ in rng b₁ & b₃ = (len b₁) - (b₂ .. b₁) holds
dom (b₁ |-- b₂) = Seg b₃

proof end;

theorem Th58: :: FINSEQ_4:58

for b₁ being FinSequence
for b₂ being set
for b₃ being Nat st b₂ in rng b₁ & b₃ in dom (b₁ |-- b₂) holds
b₃ + (b₂ .. b₁) in dom b₁

proof end;

theorem Th59: :: FINSEQ_4:59

for b₁ being FinSequence
for b₂ being set st b₂ in rng b₁ holds
rng (b₁ |-- b₂) c= rng b₁

proof end;

theorem Th60: :: FINSEQ_4:60

for b₁ being FinSequence
for b₂ being set holds
( b₁ just_once_values b₂ iff ( b₂ in rng b₁ & not b₂ in rng (b₁ |-- b₂) ) )

proof end;

theorem Th61: :: FINSEQ_4:61

for b₁ being FinSequence
for b₂ being set st b₂ in rng b₁ & b₁ is one-to-one holds
not b₂ in rng (b₁ |-- b₂)

proof end;

theorem Th62: :: FINSEQ_4:62

for b₁ being FinSequence
for b₂ being set holds
( b₁ just_once_values b₂ iff ( b₂ in rng b₁ & rng (b₁ |-- b₂) misses {b₂} ) )

proof end;

theorem Th63: :: FINSEQ_4:63

for b₁ being FinSequence
for b₂ being set st b₂ in rng b₁ & b₁ is one-to-one holds
rng (b₁ |-- b₂) misses {b₂}

proof end;

theorem Th64: :: FINSEQ_4:64

for b₁ being FinSequence
for b₂ being set st b₂ in rng b₁ holds
( b₂ .. b₁ = len b₁ iff b₁ |-- b₂ = {} )

proof end;

theorem Th65: :: FINSEQ_4:65

for b₁ being FinSequence
for b₂ being set
for b₃ being non empty set st b₂ in rng b₁ & b₁ is FinSequence of b₃ holds
b₁ |-- b₂ is FinSequence of b₃

proof end;

theorem Th66: :: FINSEQ_4:66

for b₁ being FinSequence
for b₂ being set st b₂ in rng b₁ holds
b₁ = ((b₁ -| b₂) ^ <*b₂*>) ^ (b₁ |-- b₂)

proof end;

theorem Th67: :: FINSEQ_4:67

for b₁ being FinSequence
for b₂ being set st b₂ in rng b₁ & b₁ is one-to-one holds
b₁ -| b₂ is one-to-one

proof end;

theorem Th68: :: FINSEQ_4:68

for b₁ being FinSequence
for b₂ being set st b₂ in rng b₁ & b₁ is one-to-one holds
b₁ |-- b₂ is one-to-one

proof end;

theorem Th69: :: FINSEQ_4:69

for b₁ being FinSequence
for b₂ being set holds
( b₁ just_once_values b₂ iff ( b₂ in rng b₁ & b₁ - {b₂} = (b₁ -| b₂) ^ (b₁ |-- b₂) ) )

proof end;

theorem Th70: :: FINSEQ_4:70

for b₁ being FinSequence
for b₂ being set st b₂ in rng b₁ & b₁ is one-to-one holds
b₁ - {b₂} = (b₁ -| b₂) ^ (b₁ |-- b₂)

proof end;

theorem Th71: :: FINSEQ_4:71

for b₁ being FinSequence
for b₂ being set st b₂ in rng b₁ & b₁ - {b₂} is one-to-one & b₁ - {b₂} = (b₁ -| b₂) ^ (b₁ |-- b₂) holds
b₁ is one-to-one

proof end;

theorem Th72: :: FINSEQ_4:72

for b₁ being FinSequence
for b₂ being set st b₂ in rng b₁ & b₁ is one-to-one holds
rng (b₁ -| b₂) misses rng (b₁ |-- b₂)

proof end;

theorem Th73: :: FINSEQ_4:73

for b₁ being set st b₁ is finite holds
ex b₂ being FinSequence st
( rng b₂ = b₁ & b₂ is one-to-one )

proof end;

theorem Th74: :: FINSEQ_4:74

for b₁ being FinSequence st rng b₁ c= dom b₁ & b₁ is one-to-one holds
rng b₁ = dom b₁

proof end;

theorem Th75: :: FINSEQ_4:75

for b₁ being FinSequence st rng b₁ = dom b₁ holds
b₁ is one-to-one

proof end;

theorem Th76: :: FINSEQ_4:76

for b₁, b₂ being FinSequence st rng b₁ = rng b₂ & len b₁ = len b₂ & b₂ is one-to-one holds
b₁ is one-to-one

proof end;

Lemma43: for b₁, b₂ being finite set
for b₃ being Function of b₁,b₂ st card b₁ = card b₂ & rng b₃ = b₂ holds
b₃ is one-to-one

proof end;

theorem Th77: :: FINSEQ_4:77

for b₁ being FinSequence holds
( b₁ is one-to-one iff card (rng b₁) = len b₁ )

proof end;

theorem Th78: :: FINSEQ_4:78

for b₁, b₂ being finite set
for b₃ being Function of b₁,b₂ st card b₁ = card b₂ & b₃ is one-to-one holds
rng b₃ = b₂

proof end;

theorem Th79: :: FINSEQ_4:79

for b₁, b₂ being finite set
for b₃ being Function of b₁,b₂ st card b₁ = card b₂ & rng b₃ = b₂ holds
b₃ is one-to-one by Lemma43;

theorem Th80: :: FINSEQ_4:80

for b₁, b₂ being set
for b₃ being Function of b₂,b₁ st Card b₁ <` Card b₂ & b₁ <> {} holds
ex b₄, b₅ being set st
( b₄ in b₂ & b₅ in b₂ & b₄ <> b₅ & b₃ . b₄ = b₃ . b₅ )

proof end;

theorem Th81: :: FINSEQ_4:81

for b₁, b₂ being set
for b₃ being Function of b₁,b₂ st Card b₁ <` Card b₂ holds
ex b₄ being set st
( b₄ in b₂ & ( for b₅ being set st b₅ in b₁ holds
b₃ . b₅ <> b₄ ) )

proof end;

theorem Th82: :: FINSEQ_4:82

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃ being Element of b₁ holds (b₂ ^ <*b₃*>) /. ((len b₂) + 1) = b₃

proof end;

theorem Th83: :: FINSEQ_4:83

for b₁ being Nat
for b₂ being non empty set
for b₃, b₄ being FinSequence of b₂ st b₁ in dom b₃ holds
(b₃ ^ b₄) /. b₁ = b₃ /. b₁

proof end;

theorem Th84: :: FINSEQ_4:84

for b₁ being Nat
for b₂ being non empty set
for b₃, b₄ being FinSequence of b₂ st b₁ in dom b₄ holds
(b₃ ^ b₄) /. ((len b₃) + b₁) = b₄ /. b₁

proof end;

theorem Th85: :: FINSEQ_4:85

for b₁ being Nat
for b₂ being natural number
for b₃ being set
for b₄ being FinSequence of b₃ st b₂ in dom (b₄ | b₁) holds
(b₄ | b₁) /. b₂ = b₄ /. b₂

proof end;

theorem Th86: :: FINSEQ_4:86

for b₁ being set
for b₂ being FinSequence of b₁
for b₃, b₄ being Nat st b₃ in dom b₂ & b₄ in Seg b₃ holds
( b₄ in dom b₂ & (b₂ | b₃) /. b₄ = b₂ /. b₄ )

proof end;