:: by Wojciech A. Trybulec

::

:: Received April 8, 1990

:: Copyright (c) 1990-2016 Association of Mizar Users

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

for f being Function

for x being object holds

( f is_one-to-one_at x iff f " (Im (f,x)) = {x} );

for f being Function

for x being object holds

( f is_one-to-one_at x iff f " (Im (f,x)) = {x} );

theorem Th2: :: FINSEQ_4:2

for f being Function

for x being object holds

( f is_one-to-one_at x iff ( x in dom f & f " {(f . x)} = {x} ) )

for x being object holds

( f is_one-to-one_at x iff ( x in dom f & f " {(f . x)} = {x} ) )

proof end;

theorem Th3: :: FINSEQ_4:3

for f being Function

for x being object holds

( f is_one-to-one_at x iff ( x in dom f & ( for z being object st z in dom f & x <> z holds

f . x <> f . z ) ) )

for x being object holds

( f is_one-to-one_at x iff ( x in dom f & ( for z being object st z in dom f & x <> z holds

f . x <> f . z ) ) )

proof end;

theorem :: FINSEQ_4:4

for f being Function holds

( ( for x being object st x in dom f holds

f is_one-to-one_at x ) iff f is one-to-one )

( ( for x being object st x in dom f holds

f is_one-to-one_at x ) iff f is one-to-one )

proof end;

:: deftheorem Def2 defines just_once_values FINSEQ_4:def 2 :

for R being Relation

for y being object holds

( R just_once_values y iff card (Coim (R,y)) = 1 );

for R being Relation

for y being object holds

( R just_once_values y iff card (Coim (R,y)) = 1 );

theorem Th7: :: FINSEQ_4:7

for f being Function

for y being object holds

( f just_once_values y iff ex x being object st

( x in dom f & y = f . x & ( for z being object st z in dom f & z <> x holds

f . z <> y ) ) )

for y being object holds

( f just_once_values y iff ex x being object st

( x in dom f & y = f . x & ( for z being object st z in dom f & z <> x holds

f . z <> y ) ) )

proof end;

theorem Th8: :: FINSEQ_4:8

for f being Function holds

( f is one-to-one iff for y being object st y in rng f holds

f just_once_values y )

( f is one-to-one iff for y being object st y in rng f holds

f just_once_values y )

proof end;

theorem Th9: :: FINSEQ_4:9

for f being Function

for x being object holds

( f is_one-to-one_at x iff ( x in dom f & f just_once_values f . x ) )

for x being object holds

( f is_one-to-one_at x iff ( x in dom f & f just_once_values f . x ) )

proof end;

definition

let f be Function;

let y be object ;

assume A1: f just_once_values y ;

existence

ex b_{1} being set st

( b_{1} in dom f & f . b_{1} = y )

for b_{1}, b_{2} being set st b_{1} in dom f & f . b_{1} = y & b_{2} in dom f & f . b_{2} = y holds

b_{1} = b_{2}

end;
let y be object ;

assume A1: f just_once_values y ;

existence

ex b

( b

proof end;

uniqueness for b

b

proof end;

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

for f being Function

for y being object st f just_once_values y holds

for b_{3} being set holds

( b_{3} = f <- y iff ( b_{3} in dom f & f . b_{3} = y ) );

for f being Function

for y being object st f just_once_values y holds

for b

( b

definition

let D be non empty set ;

let d1, d2 be Element of D;

:: original: <*

redefine func <*d1,d2*> -> FinSequence of D;

coherence

<*d1,d2*> is FinSequence of D by FINSEQ_2:13;

end;
let d1, d2 be Element of D;

:: original: <*

redefine func <*d1,d2*> -> FinSequence of D;

coherence

<*d1,d2*> is FinSequence of D by FINSEQ_2:13;

definition

let D be non empty set ;

let d1, d2, d3 be Element of D;

:: original: <*

redefine func <*d1,d2,d3*> -> FinSequence of D;

coherence

<*d1,d2,d3*> is FinSequence of D by FINSEQ_2:14;

end;
let d1, d2, d3 be Element of D;

:: original: <*

redefine func <*d1,d2,d3*> -> FinSequence of D;

coherence

<*d1,d2,d3*> is FinSequence of D by FINSEQ_2:14;

theorem :: FINSEQ_4:15

for i being Nat

for D being set

for P being FinSequence of D st 1 <= i & i <= len P holds

P /. i = P . i

for D being set

for P being FinSequence of D st 1 <= i & i <= len P holds

P /. i = P . i

proof end;

theorem :: FINSEQ_4:17

for D being non empty set

for d1, d2 being Element of D holds

( <*d1,d2*> /. 1 = d1 & <*d1,d2*> /. 2 = d2 )

for d1, d2 being Element of D holds

( <*d1,d2*> /. 1 = d1 & <*d1,d2*> /. 2 = d2 )

proof end;

theorem :: FINSEQ_4:18

for D being non empty set

for d1, d2, d3 being Element of D holds

( <*d1,d2,d3*> /. 1 = d1 & <*d1,d2,d3*> /. 2 = d2 & <*d1,d2,d3*> /. 3 = d3 )

for d1, d2, d3 being Element of D holds

( <*d1,d2,d3*> /. 1 = d1 & <*d1,d2,d3*> /. 2 = d2 & <*d1,d2,d3*> /. 3 = d3 )

proof end;

definition
end;

:: deftheorem defines .. FINSEQ_4:def 4 :

for p being FinSequence

for x being object holds x .. p = (Sgm (p " {x})) . 1;

for p being FinSequence

for x being object holds x .. p = (Sgm (p " {x})) . 1;

theorem Th22: :: FINSEQ_4:22

for p being FinSequence

for x being object st x in rng p holds

( (x .. p) - 1 is Element of NAT & (len p) - (x .. p) is Element of NAT )

for x being object st x in rng p holds

( (x .. p) - 1 is Element of NAT & (len p) - (x .. p) is Element of NAT )

proof end;

theorem Th24: :: FINSEQ_4:24

for p being FinSequence

for x being object

for k being Nat st k in dom p & k < x .. p holds

p . k <> x

for x being object

for k being Nat st k in dom p & k < x .. p holds

p . k <> x

proof end;

theorem Th26: :: FINSEQ_4:26

for p being FinSequence

for x being object st p just_once_values x holds

for k being Nat st k in dom p & k <> x .. p holds

p . k <> x

for x being object st p just_once_values x holds

for k being Nat st k in dom p & k <> x .. p holds

p . k <> x

proof end;

theorem Th27: :: FINSEQ_4:27

for p being FinSequence

for x being object st x in rng p & ( for k being Nat st k in dom p & k <> x .. p holds

p . k <> x ) holds

p just_once_values x

for x being object st x in rng p & ( for k being Nat st k in dom p & k <> x .. p holds

p . k <> x ) holds

p just_once_values x

proof end;

theorem :: FINSEQ_4:28

for p being FinSequence

for x being object holds

( p just_once_values x iff ( x in rng p & {(x .. p)} = p " {x} ) )

for x being object holds

( p just_once_values x iff ( x in rng p & {(x .. p)} = p " {x} ) )

proof end;

theorem :: FINSEQ_4:29

for p being FinSequence

for x being object st p is one-to-one & x in rng p holds

{(x .. p)} = p " {x}

for x being object st p is one-to-one & x in rng p holds

{(x .. p)} = p " {x}

proof end;

theorem Th30: :: FINSEQ_4:30

for p being FinSequence

for x being object holds

( p just_once_values x iff len (p - {x}) = (len p) - 1 )

for x being object holds

( p just_once_values x iff len (p - {x}) = (len p) - 1 )

proof end;

theorem Th31: :: FINSEQ_4:31

for p being FinSequence

for x being object st p just_once_values x holds

for k being Nat st k in dom (p - {x}) holds

( ( k < x .. p implies (p - {x}) . k = p . k ) & ( x .. p <= k implies (p - {x}) . k = p . (k + 1) ) )

for x being object st p just_once_values x holds

for k being Nat st k in dom (p - {x}) holds

( ( k < x .. p implies (p - {x}) . k = p . k ) & ( x .. p <= k implies (p - {x}) . k = p . (k + 1) ) )

proof end;

theorem :: FINSEQ_4:32

for p being FinSequence

for x being object st p is one-to-one & x in rng p holds

for k being Nat st k in dom (p - {x}) holds

( ( (p - {x}) . k = p . k implies k < x .. p ) & ( k < x .. p implies (p - {x}) . k = p . k ) & ( (p - {x}) . k = p . (k + 1) implies x .. p <= k ) & ( x .. p <= k implies (p - {x}) . k = p . (k + 1) ) )

for x being object st p is one-to-one & x in rng p holds

for k being Nat st k in dom (p - {x}) holds

( ( (p - {x}) . k = p . k implies k < x .. p ) & ( k < x .. p implies (p - {x}) . k = p . k ) & ( (p - {x}) . k = p . (k + 1) implies x .. p <= k ) & ( x .. p <= k implies (p - {x}) . k = p . (k + 1) ) )

proof end;

definition

let p be FinSequence;

let x be object ;

assume A1: x in rng p ;

ex b_{1} being FinSequence ex n being Nat st

( n = (x .. p) - 1 & b_{1} = p | (Seg n) )

for b_{1}, b_{2} being FinSequence st ex n being Nat st

( n = (x .. p) - 1 & b_{1} = p | (Seg n) ) & ex n being Nat st

( n = (x .. p) - 1 & b_{2} = p | (Seg n) ) holds

b_{1} = b_{2}
;

end;
let x be object ;

assume A1: x in rng p ;

func p -| x -> FinSequence means :Def5: :: FINSEQ_4:def 5

ex n being Nat st

( n = (x .. p) - 1 & it = p | (Seg n) );

existence ex n being Nat st

( n = (x .. p) - 1 & it = p | (Seg n) );

ex b

( n = (x .. p) - 1 & b

proof end;

uniqueness for b

( n = (x .. p) - 1 & b

( n = (x .. p) - 1 & b

b

:: deftheorem Def5 defines -| FINSEQ_4:def 5 :

for p being FinSequence

for x being object st x in rng p holds

for b_{3} being FinSequence holds

( b_{3} = p -| x iff ex n being Nat st

( n = (x .. p) - 1 & b_{3} = p | (Seg n) ) );

for p being FinSequence

for x being object st x in rng p holds

for b

( b

( n = (x .. p) - 1 & b

theorem Th33: :: FINSEQ_4:33

for p being FinSequence

for x being object

for n being Nat st x in rng p & n = (x .. p) - 1 holds

p | (Seg n) = p -| x

for x being object

for n being Nat st x in rng p & n = (x .. p) - 1 holds

p | (Seg n) = p -| x

proof end;

theorem Th35: :: FINSEQ_4:35

for p being FinSequence

for x being object

for n being Nat st x in rng p & n = (x .. p) - 1 holds

dom (p -| x) = Seg n

for x being object

for n being Nat st x in rng p & n = (x .. p) - 1 holds

dom (p -| x) = Seg n

proof end;

theorem Th36: :: FINSEQ_4:36

for p being FinSequence

for x being object

for k being Nat st x in rng p & k in dom (p -| x) holds

p . k = (p -| x) . k

for x being object

for k being Nat st x in rng p & k in dom (p -| x) holds

p . k = (p -| x) . k

proof end;

theorem :: FINSEQ_4:41

for p being FinSequence

for x being object

for D being non empty set st x in rng p & p is FinSequence of D holds

p -| x is FinSequence of D

for x being object

for D being non empty set st x in rng p & p is FinSequence of D holds

p -| x is FinSequence of D

proof end;

definition

let p be FinSequence;

let x be object ;

assume A1: x in rng p ;

ex b_{1} being FinSequence st

( len b_{1} = (len p) - (x .. p) & ( for k being Nat st k in dom b_{1} holds

b_{1} . k = p . (k + (x .. p)) ) )

for b_{1}, b_{2} being FinSequence st len b_{1} = (len p) - (x .. p) & ( for k being Nat st k in dom b_{1} holds

b_{1} . k = p . (k + (x .. p)) ) & len b_{2} = (len p) - (x .. p) & ( for k being Nat st k in dom b_{2} holds

b_{2} . k = p . (k + (x .. p)) ) holds

b_{1} = b_{2}

end;
let x be object ;

assume A1: x in rng p ;

func p |-- x -> FinSequence means :Def6: :: FINSEQ_4:def 6

( len it = (len p) - (x .. p) & ( for k being Nat st k in dom it holds

it . k = p . (k + (x .. p)) ) );

existence ( len it = (len p) - (x .. p) & ( for k being Nat st k in dom it holds

it . k = p . (k + (x .. p)) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

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

for p being FinSequence

for x being object st x in rng p holds

for b_{3} being FinSequence holds

( b_{3} = p |-- x iff ( len b_{3} = (len p) - (x .. p) & ( for k being Nat st k in dom b_{3} holds

b_{3} . k = p . (k + (x .. p)) ) ) );

for p being FinSequence

for x being object st x in rng p holds

for b

( b

b

theorem Th42: :: FINSEQ_4:42

for p being FinSequence

for x being object

for n being Nat st x in rng p & n = (len p) - (x .. p) holds

dom (p |-- x) = Seg n

for x being object

for n being Nat st x in rng p & n = (len p) - (x .. p) holds

dom (p |-- x) = Seg n

proof end;

theorem Th43: :: FINSEQ_4:43

for p being FinSequence

for x being object

for n being Nat st x in rng p & n in dom (p |-- x) holds

n + (x .. p) in dom p

for x being object

for n being Nat st x in rng p & n in dom (p |-- x) holds

n + (x .. p) in dom p

proof end;

theorem Th45: :: FINSEQ_4:45

for p being FinSequence

for x being object holds

( p just_once_values x iff ( x in rng p & not x in rng (p |-- x) ) )

for x being object holds

( p just_once_values x iff ( x in rng p & not x in rng (p |-- x) ) )

proof end;

theorem Th46: :: FINSEQ_4:46

for p being FinSequence

for x being object st x in rng p & p is one-to-one holds

not x in rng (p |-- x)

for x being object st x in rng p & p is one-to-one holds

not x in rng (p |-- x)

proof end;

theorem :: FINSEQ_4:47

for p being FinSequence

for x being object holds

( p just_once_values x iff ( x in rng p & rng (p |-- x) misses {x} ) )

for x being object holds

( p just_once_values x iff ( x in rng p & rng (p |-- x) misses {x} ) )

proof end;

theorem :: FINSEQ_4:48

for p being FinSequence

for x being object st x in rng p & p is one-to-one holds

rng (p |-- x) misses {x}

for x being object st x in rng p & p is one-to-one holds

rng (p |-- x) misses {x}

proof end;

theorem :: FINSEQ_4:50

for p being FinSequence

for x being object

for D being non empty set st x in rng p & p is FinSequence of D holds

p |-- x is FinSequence of D

for x being object

for D being non empty set st x in rng p & p is FinSequence of D holds

p |-- x is FinSequence of D

proof end;

theorem :: FINSEQ_4:52

for p being FinSequence

for x being object st x in rng p & p is one-to-one holds

p -| x is one-to-one

for x being object st x in rng p & p is one-to-one holds

p -| x is one-to-one

proof end;

theorem :: FINSEQ_4:53

for p being FinSequence

for x being object st x in rng p & p is one-to-one holds

p |-- x is one-to-one

for x being object st x in rng p & p is one-to-one holds

p |-- x is one-to-one

proof end;

theorem Th54: :: FINSEQ_4:54

for p being FinSequence

for x being object holds

( p just_once_values x iff ( x in rng p & p - {x} = (p -| x) ^ (p |-- x) ) )

for x being object holds

( p just_once_values x iff ( x in rng p & p - {x} = (p -| x) ^ (p |-- x) ) )

proof end;

theorem :: FINSEQ_4:55

for p being FinSequence

for x being object st x in rng p & p is one-to-one holds

p - {x} = (p -| x) ^ (p |-- x)

for x being object st x in rng p & p is one-to-one holds

p - {x} = (p -| x) ^ (p |-- x)

proof end;

theorem Th56: :: FINSEQ_4:56

for p being FinSequence

for x being object st x in rng p & p - {x} is one-to-one & p - {x} = (p -| x) ^ (p |-- x) holds

p is one-to-one

for x being object st x in rng p & p - {x} is one-to-one & p - {x} = (p -| x) ^ (p |-- x) holds

p is one-to-one

proof end;

theorem :: FINSEQ_4:57

for p being FinSequence

for x being object st x in rng p & p is one-to-one holds

rng (p -| x) misses rng (p |-- x)

for x being object st x in rng p & p is one-to-one holds

rng (p -| x) misses rng (p |-- x)

proof end;

Lm1: for A, B being finite set

for f being Function of A,B st card A = card B & rng f = B holds

f is one-to-one

proof end;

theorem :: FINSEQ_4:63

for A, B being finite set

for f being Function of A,B st card A = card B & f is one-to-one holds

rng f = B

for f being Function of A,B st card A = card B & f is one-to-one holds

rng f = B

proof end;

theorem :: FINSEQ_4:64

theorem :: FINSEQ_4:65

for A, B being set

for f being Function of A,B st card B in card A & B <> {} holds

ex x, y being object st

( x in A & y in A & x <> y & f . x = f . y )

for f being Function of A,B st card B in card A & B <> {} holds

ex x, y being object st

( x in A & y in A & x <> y & f . x = f . y )

proof end;

theorem Th66: :: FINSEQ_4:66

for A, B being set

for f being Function of A,B st card A in card B holds

ex x being object st

( x in B & ( for y being object st y in A holds

f . y <> x ) )

for f being Function of A,B st card A in card B holds

ex x being object st

( x in B & ( for y being object st y in A holds

f . y <> x ) )

proof end;

:: from TOPREAL4

theorem :: FINSEQ_4:67

for D being non empty set

for f being FinSequence of D

for p being Element of D holds (f ^ <*p*>) /. ((len f) + 1) = p

for f being FinSequence of D

for p being Element of D holds (f ^ <*p*>) /. ((len f) + 1) = p

proof end;

:: from GROUP_5

theorem :: FINSEQ_4:68

for k being Nat

for E being non empty set

for p, q being FinSequence of E st k in dom p holds

(p ^ q) /. k = p /. k

for E being non empty set

for p, q being FinSequence of E st k in dom p holds

(p ^ q) /. k = p /. k

proof end;

theorem :: FINSEQ_4:69

for k being Nat

for E being non empty set

for p, q being FinSequence of E st k in dom q holds

(p ^ q) /. ((len p) + k) = q /. k

for E being non empty set

for p, q being FinSequence of E st k in dom q holds

(p ^ q) /. ((len p) + k) = q /. k

proof end;

:: from TOPREAL1

theorem :: FINSEQ_4:70

for a, m being Nat

for D being set

for p being FinSequence of D st a in dom (p | m) holds

(p | m) /. a = p /. a

for D being set

for p being FinSequence of D st a in dom (p | m) holds

(p | m) /. a = p /. a

proof end;

:: from GOBOARD1

theorem Th71: :: FINSEQ_4:71

for D being set

for f being FinSequence of D

for n, m being Nat st n in dom f & m in Seg n holds

( m in dom f & (f | n) /. m = f /. m )

for f being FinSequence of D

for n, m being Nat st n in dom f & m in Seg n holds

( m in dom f & (f | n) /. m = f /. m )

proof end;

:: from VECTSP_9, 2006.01.06, A.T.

theorem :: FINSEQ_4:72

for n being Nat

for X being finite set st n <= card X holds

ex A being finite Subset of X st card A = n

for X being finite set st n <= card X holds

ex A being finite Subset of X st card A = n

proof end;

theorem :: FINSEQ_4:73

:: form SCMPDS_1, 2006.03.24, A.T.

definition

let x1, x2, x3, x4 be object ;

correctness

coherence

<*x1,x2,x3*> ^ <*x4*> is set ;

;

let x5 be object ;

correctness

coherence

<*x1,x2,x3*> ^ <*x4,x5*> is set ;

;

end;
correctness

coherence

<*x1,x2,x3*> ^ <*x4*> is set ;

;

let x5 be object ;

correctness

coherence

<*x1,x2,x3*> ^ <*x4,x5*> is set ;

;

:: deftheorem defines <* FINSEQ_4:def 7 :

for x1, x2, x3, x4 being object holds <*x1,x2,x3,x4*> = <*x1,x2,x3*> ^ <*x4*>;

for x1, x2, x3, x4 being object holds <*x1,x2,x3,x4*> = <*x1,x2,x3*> ^ <*x4*>;

:: deftheorem defines <* FINSEQ_4:def 8 :

for x1, x2, x3, x4, x5 being object holds <*x1,x2,x3,x4,x5*> = <*x1,x2,x3*> ^ <*x4,x5*>;

for x1, x2, x3, x4, x5 being object holds <*x1,x2,x3,x4,x5*> = <*x1,x2,x3*> ^ <*x4,x5*>;

registration

let x1, x2, x3, x4 be object ;

coherence

( not <*x1,x2,x3,x4*> is empty & <*x1,x2,x3,x4*> is Function-like & <*x1,x2,x3,x4*> is Relation-like ) ;

let x5 be object ;

coherence

( not <*x1,x2,x3,x4,x5*> is empty & <*x1,x2,x3,x4,x5*> is Function-like & <*x1,x2,x3,x4,x5*> is Relation-like ) ;

end;
coherence

( not <*x1,x2,x3,x4*> is empty & <*x1,x2,x3,x4*> is Function-like & <*x1,x2,x3,x4*> is Relation-like ) ;

let x5 be object ;

coherence

( not <*x1,x2,x3,x4,x5*> is empty & <*x1,x2,x3,x4,x5*> is Function-like & <*x1,x2,x3,x4,x5*> is Relation-like ) ;

registration

let x1, x2, x3, x4 be object ;

coherence

<*x1,x2,x3,x4*> is FinSequence-like ;

let x5 be object ;

coherence

<*x1,x2,x3,x4,x5*> is FinSequence-like ;

end;
coherence

<*x1,x2,x3,x4*> is FinSequence-like ;

let x5 be object ;

coherence

<*x1,x2,x3,x4,x5*> is FinSequence-like ;

definition

let D be non empty set ;

let x1, x2, x3, x4 be Element of D;

:: original: <*

redefine func <*x1,x2,x3,x4*> -> FinSequence of D;

coherence

<*x1,x2,x3,x4*> is FinSequence of D

end;
let x1, x2, x3, x4 be Element of D;

:: original: <*

redefine func <*x1,x2,x3,x4*> -> FinSequence of D;

coherence

<*x1,x2,x3,x4*> is FinSequence of D

proof end;

definition

let D be non empty set ;

let x1, x2, x3, x4, x5 be Element of D;

:: original: <*

redefine func <*x1,x2,x3,x4,x5*> -> FinSequence of D;

coherence

<*x1,x2,x3,x4,x5*> is FinSequence of D

end;
let x1, x2, x3, x4, x5 be Element of D;

:: original: <*

redefine func <*x1,x2,x3,x4,x5*> -> FinSequence of D;

coherence

<*x1,x2,x3,x4,x5*> is FinSequence of D

proof end;

theorem Th74: :: FINSEQ_4:74

for x1, x2, x3, x4 being object holds

( <*x1,x2,x3,x4*> = <*x1,x2,x3*> ^ <*x4*> & <*x1,x2,x3,x4*> = <*x1,x2*> ^ <*x3,x4*> & <*x1,x2,x3,x4*> = <*x1*> ^ <*x2,x3,x4*> & <*x1,x2,x3,x4*> = ((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*> )

( <*x1,x2,x3,x4*> = <*x1,x2,x3*> ^ <*x4*> & <*x1,x2,x3,x4*> = <*x1,x2*> ^ <*x3,x4*> & <*x1,x2,x3,x4*> = <*x1*> ^ <*x2,x3,x4*> & <*x1,x2,x3,x4*> = ((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*> )

proof end;

theorem Th75: :: FINSEQ_4:75

for x1, x2, x3, x4, x5 being object holds

( <*x1,x2,x3,x4,x5*> = <*x1,x2,x3*> ^ <*x4,x5*> & <*x1,x2,x3,x4,x5*> = <*x1,x2,x3,x4*> ^ <*x5*> & <*x1,x2,x3,x4,x5*> = (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*> & <*x1,x2,x3,x4,x5*> = <*x1,x2*> ^ <*x3,x4,x5*> & <*x1,x2,x3,x4,x5*> = <*x1*> ^ <*x2,x3,x4,x5*> )

( <*x1,x2,x3,x4,x5*> = <*x1,x2,x3*> ^ <*x4,x5*> & <*x1,x2,x3,x4,x5*> = <*x1,x2,x3,x4*> ^ <*x5*> & <*x1,x2,x3,x4,x5*> = (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*> & <*x1,x2,x3,x4,x5*> = <*x1,x2*> ^ <*x3,x4,x5*> & <*x1,x2,x3,x4,x5*> = <*x1*> ^ <*x2,x3,x4,x5*> )

proof end;

theorem Th76: :: FINSEQ_4:76

for x1, x2, x3, x4 being object

for p being FinSequence holds

( p = <*x1,x2,x3,x4*> iff ( len p = 4 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 ) )

for p being FinSequence holds

( p = <*x1,x2,x3,x4*> iff ( len p = 4 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 ) )

proof end;

::$CT

theorem Th77: :: FINSEQ_4:78

for x1, x2, x3, x4, x5 being object

for p being FinSequence holds

( p = <*x1,x2,x3,x4,x5*> iff ( len p = 5 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 ) )

for p being FinSequence holds

( p = <*x1,x2,x3,x4,x5*> iff ( len p = 5 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 ) )

proof end;

::$CT

theorem :: FINSEQ_4:80

for ND being non empty set

for y1, y2, y3, y4 being Element of ND holds

( <*y1,y2,y3,y4*> /. 1 = y1 & <*y1,y2,y3,y4*> /. 2 = y2 & <*y1,y2,y3,y4*> /. 3 = y3 & <*y1,y2,y3,y4*> /. 4 = y4 )

for y1, y2, y3, y4 being Element of ND holds

( <*y1,y2,y3,y4*> /. 1 = y1 & <*y1,y2,y3,y4*> /. 2 = y2 & <*y1,y2,y3,y4*> /. 3 = y3 & <*y1,y2,y3,y4*> /. 4 = y4 )

proof end;

theorem :: FINSEQ_4:81

for ND being non empty set

for y1, y2, y3, y4, y5 being Element of ND holds

( <*y1,y2,y3,y4,y5*> /. 1 = y1 & <*y1,y2,y3,y4,y5*> /. 2 = y2 & <*y1,y2,y3,y4,y5*> /. 3 = y3 & <*y1,y2,y3,y4,y5*> /. 4 = y4 & <*y1,y2,y3,y4,y5*> /. 5 = y5 )

for y1, y2, y3, y4, y5 being Element of ND holds

( <*y1,y2,y3,y4,y5*> /. 1 = y1 & <*y1,y2,y3,y4,y5*> /. 2 = y2 & <*y1,y2,y3,y4,y5*> /. 3 = y3 & <*y1,y2,y3,y4,y5*> /. 4 = y4 & <*y1,y2,y3,y4,y5*> /. 5 = y5 )

proof end;

:: form SCMFSA_7, 2007.07.22, A.T.

theorem Th80: :: FINSEQ_4:82

for D being non empty set

for p, q being FinSequence of D st p c= q holds

ex p9 being FinSequence of D st p ^ p9 = q

for p, q being FinSequence of D st p c= q holds

ex p9 being FinSequence of D st p ^ p9 = q

proof end;

theorem :: FINSEQ_4:83

for D being non empty set

for p, q being FinSequence of D

for i being Element of NAT st p c= q & 1 <= i & i <= len p holds

q . i = p . i

for p, q being FinSequence of D

for i being Element of NAT st p c= q & 1 <= i & i <= len p holds

q . i = p . i

proof end;

:: from CIRCCMB3, 2009.02.16, A.T.

registration

let x1, x2, x3, x4 be object ;

coherence

<*x1,x2,x3,x4*> is 4 -element ;

let x5 be object ;

coherence

<*x1,x2,x3,x4,x5*> is 5 -element ;

end;
coherence

<*x1,x2,x3,x4*> is 4 -element ;

let x5 be object ;

coherence

<*x1,x2,x3,x4,x5*> is 5 -element ;

theorem :: FINSEQ_4:85

for S being set

for D1, D2 being non empty set

for f1 being Function of S,D1

for f2 being Function of D1,D2 st f1 is bijective & f2 is bijective holds

f2 * f1 is bijective

for D1, D2 being non empty set

for f1 being Function of S,D1

for f2 being Function of D1,D2 st f1 is bijective & f2 is bijective holds

f2 * f1 is bijective

proof end;

:: Partitions & Equivalence Relations

registration
end;

registration

let X be non empty finite set ;

existence

ex b_{1} being a_partition of X st

( not b_{1} is empty & b_{1} is finite )

end;
existence

ex b

( not b

proof end;

theorem Th85: :: FINSEQ_4:87

for X being non empty set

for PX being a_partition of X

for Pi being set st Pi in PX holds

ex x being Element of X st x in Pi

for PX being a_partition of X

for Pi being set st Pi in PX holds

ex x being Element of X st x in Pi

proof end;

theorem :: FINSEQ_4:89

for A being non empty finite set

for PA1, PA2 being a_partition of A st PA1 is_finer_than PA2 holds

card PA2 <= card PA1

for PA1, PA2 being a_partition of A st PA1 is_finer_than PA2 holds

card PA2 <= card PA1

proof end;

theorem Th88: :: FINSEQ_4:90

for A being non empty finite set

for PA1, PA2 being a_partition of A st PA1 is_finer_than PA2 holds

for p2 being Element of PA2 ex p1 being Element of PA1 st p1 c= p2

for PA1, PA2 being a_partition of A st PA1 is_finer_than PA2 holds

for p2 being Element of PA2 ex p1 being Element of PA1 st p1 c= p2

proof end;

theorem :: FINSEQ_4:91

for A being non empty finite set

for PA1, PA2 being a_partition of A st PA1 is_finer_than PA2 & card PA1 = card PA2 holds

PA1 = PA2

for PA1, PA2 being a_partition of A st PA1 is_finer_than PA2 & card PA1 = card PA2 holds

PA1 = PA2

proof end;

registration

let D be set ;

let M be FinSequence of D * ;

let k be Nat;

coherence

( M /. k is Function-like & M /. k is Relation-like ) ;

end;
let M be FinSequence of D * ;

let k be Nat;

coherence

( M /. k is Function-like & M /. k is Relation-like ) ;

registration

let D be set ;

let M be FinSequence of D * ;

let k be Nat;

coherence

for b_{1} being Function st b_{1} = M /. k holds

( b_{1} is FinSequence-like & b_{1} is D -valued )
by FINSEQ_1:def 11;

end;
let M be FinSequence of D * ;

let k be Nat;

coherence

for b

( b

theorem :: FINSEQ_4:92

for m being Nat

for D being non empty set

for f being FinSequence of D st m in dom f holds

f /. 1 = (f | m) /. 1

for D being non empty set

for f being FinSequence of D st m in dom f holds

f /. 1 = (f | m) /. 1

proof end;

theorem :: FINSEQ_4:93

for m being Nat

for D being non empty set

for f being FinSequence of D st m in dom f holds

f /. m = (f | m) /. (len (f | m))

for D being non empty set

for f being FinSequence of D st m in dom f holds

f /. m = (f | m) /. (len (f | m))

proof end;

:: Pigeon Hole Principle