:: by Grzegorz Bancerek and Andrzej Trybulec

::

:: Received January 12, 1996

:: Copyright (c) 1996-2012 Association of Mizar Users

begin

theorem :: FUNCT_7:2

for X being set

for Y being non empty set

for f being Function of X,Y st f is one-to-one holds

for B being Subset of X

for C being Subset of Y st C c= f .: B holds

f " C c= B

for Y being non empty set

for f being Function of X,Y st f is one-to-one holds

for B being Subset of X

for C being Subset of Y st C c= f .: B holds

f " C c= B

proof end;

theorem Th3: :: FUNCT_7:3

for X, Y being non empty set

for f being Function of X,Y st f is one-to-one holds

for x being Element of X

for A being Subset of X st f . x in f .: A holds

x in A

for f being Function of X,Y st f is one-to-one holds

for x being Element of X

for A being Subset of X st f . x in f .: A holds

x in A

proof end;

theorem Th4: :: FUNCT_7:4

for X, Y being non empty set

for f being Function of X,Y st f is one-to-one holds

for x being Element of X

for A being Subset of X

for B being Subset of Y st f . x in (f .: A) \ B holds

x in A \ (f " B)

for f being Function of X,Y st f is one-to-one holds

for x being Element of X

for A being Subset of X

for B being Subset of Y st f . x in (f .: A) \ B holds

x in A \ (f " B)

proof end;

theorem :: FUNCT_7:5

for X, Y being non empty set

for f being Function of X,Y st f is one-to-one holds

for y being Element of Y

for A being Subset of X

for B being Subset of Y st y in (f .: A) \ B holds

(f ") . y in A \ (f " B)

for f being Function of X,Y st f is one-to-one holds

for y being Element of Y

for A being Subset of X

for B being Subset of Y st y in (f .: A) \ B holds

(f ") . y in A \ (f " B)

proof end;

registration
end;

theorem Th7: :: FUNCT_7:7

for I being set

for M being ManySortedSet of I

for i being set st i in I holds

i .--> (M . i) = M | {i}

for M being ManySortedSet of I

for i being set st i in I holds

i .--> (M . i) = M | {i}

proof end;

theorem :: FUNCT_7:8

for I, J being set

for M being ManySortedSet of [:I,J:]

for i, j being set st i in I & j in J holds

(i,j) :-> (M . (i,j)) = M | [:{i},{j}:]

for M being ManySortedSet of [:I,J:]

for i, j being set st i in I & j in J holds

(i,j) :-> (M . (i,j)) = M | [:{i},{j}:]

proof end;

theorem :: FUNCT_7:20

for A being Subset of NAT st ( for n, m being Element of NAT st n in A & m < n holds

m in A ) holds

A is Cardinal

m in A ) holds

A is Cardinal

proof end;

theorem :: FUNCT_7:21

for A being finite set

for X being non empty Subset-Family of A ex C being Element of X st

for B being Element of X st B c= C holds

B = C

for X being non empty Subset-Family of A ex C being Element of X st

for B being Element of X st B c= C holds

B = C

proof end;

theorem Th22: :: FUNCT_7:22

for p, q being FinSequence st len p = (len q) + 1 holds

for i being Element of NAT holds

( i in dom q iff ( i in dom p & i + 1 in dom p ) )

for i being Element of NAT holds

( i in dom q iff ( i in dom p & i + 1 in dom p ) )

proof end;

registration

ex b_{1} being FinSequence st

( b_{1} is Function-yielding & not b_{1} is empty & b_{1} is non-empty )
end;

cluster non empty Relation-like non-empty NAT -defined Function-like Function-yielding finite FinSequence-like FinSubsequence-like for set ;

existence ex b

( b

proof end;

registration

coherence

for b_{1} being Function st b_{1} is empty holds

b_{1} is Function-yielding
;

let f be Function;

coherence

<*f*> is Function-yielding

coherence

<*f,g*> is Function-yielding

coherence

<*f,g,h*> is Function-yielding

end;
for b

b

let f be Function;

coherence

<*f*> is Function-yielding

proof end;

let g be Function;coherence

<*f,g*> is Function-yielding

proof end;

let h be Function;coherence

<*f,g,h*> is Function-yielding

proof end;

registration
end;

registration
end;

theorem Th23: :: FUNCT_7:23

for p, q being FinSequence st p ^ q is Function-yielding holds

( p is Function-yielding & q is Function-yielding )

( p is Function-yielding & q is Function-yielding )

proof end;

begin

scheme :: FUNCT_7:sch 1

Kappa2D{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}() -> non empty set , F_{4}( Element of F_{1}(), Element of F_{2}()) -> set } :

Kappa2D{ F

ex f being Function of [:F_{1}(),F_{2}():],F_{3}() st

for x being Element of F_{1}()

for y being Element of F_{2}() holds f . (x,y) = F_{4}(x,y)

provided
for x being Element of F

for y being Element of F

proof end;

scheme :: FUNCT_7:sch 5

FuncSeqInd{ P_{1}[ set ] } :

provided

FuncSeqInd{ P

provided

A1:
P_{1}[ {} ]
and

A2: for p being Function-yielding FinSequence st P_{1}[p] holds

for f being Function holds P_{1}[p ^ <*f*>]

A2: for p being Function-yielding FinSequence st P

for f being Function holds P

proof end;

begin

:: deftheorem Def2 defines equal_outside FUNCT_7:def 2 :

for f, g being Function

for A being set holds

( f,g equal_outside A iff f | ((dom f) \ A) = g | ((dom g) \ A) );

for f, g being Function

for A being set holds

( f,g equal_outside A iff f | ((dom f) \ A) = g | ((dom g) \ A) );

theorem Th27: :: FUNCT_7:27

for f, g, h being Function

for A being set st f,g equal_outside A & g,h equal_outside A holds

f,h equal_outside A

for A being set st f,g equal_outside A & g,h equal_outside A holds

f,h equal_outside A

proof end;

definition

let f be Function;

let i, x be set ;

coherence

( ( i in dom f implies f +* (i .--> x) is Function ) & ( not i in dom f implies f is Function ) );

consistency

for b_{1} being Function holds verum;

;

end;
let i, x be set ;

func f +* (i,x) -> Function equals :Def3: :: FUNCT_7:def 3

f +* (i .--> x) if i in dom f

otherwise f;

correctness f +* (i .--> x) if i in dom f

otherwise f;

coherence

( ( i in dom f implies f +* (i .--> x) is Function ) & ( not i in dom f implies f is Function ) );

consistency

for b

;

:: deftheorem Def3 defines +* FUNCT_7:def 3 :

for f being Function

for i, x being set holds

( ( i in dom f implies f +* (i,x) = f +* (i .--> x) ) & ( not i in dom f implies f +* (i,x) = f ) );

for f being Function

for i, x being set holds

( ( i in dom f implies f +* (i,x) = f +* (i .--> x) ) & ( not i in dom f implies f +* (i,x) = f ) );

theorem :: FUNCT_7:33

for f being Function

for d, e, i, j being set st i <> j holds

(f +* (i,d)) +* (j,e) = (f +* (j,e)) +* (i,d)

for d, e, i, j being set st i <> j holds

(f +* (i,d)) +* (j,e) = (f +* (j,e)) +* (i,d)

proof end;

registration
end;

definition

let D be set ;

let f be FinSequence of D;

let i be Element of NAT ;

let d be Element of D;

:: original: +*

redefine func f +* (i,d) -> FinSequence of D;

coherence

f +* (i,d) is FinSequence of D

end;
let f be FinSequence of D;

let i be Element of NAT ;

let d be Element of D;

:: original: +*

redefine func f +* (i,d) -> FinSequence of D;

coherence

f +* (i,d) is FinSequence of D

proof end;

theorem :: FUNCT_7:36

for D being non empty set

for f being FinSequence of D

for d being Element of D

for i being Element of NAT st i in dom f holds

(f +* (i,d)) /. i = d

for f being FinSequence of D

for d being Element of D

for i being Element of NAT st i in dom f holds

(f +* (i,d)) /. i = d

proof end;

theorem :: FUNCT_7:37

for D being non empty set

for f being FinSequence of D

for d being Element of D

for i, j being Element of NAT st i <> j & j in dom f holds

(f +* (i,d)) /. j = f /. j

for f being FinSequence of D

for d being Element of D

for i, j being Element of NAT st i <> j & j in dom f holds

(f +* (i,d)) /. j = f /. j

proof end;

theorem :: FUNCT_7:38

for D being non empty set

for f being FinSequence of D

for d, e being Element of D

for i being Element of NAT holds f +* (i,(f /. i)) = f

for f being FinSequence of D

for d, e being Element of D

for i being Element of NAT holds f +* (i,(f /. i)) = f

proof end;

begin

definition

let X be set ;

let p be Function-yielding FinSequence;

for b_{1}, b_{2} being Function st ex f being ManySortedFunction of NAT st

( b_{1} = f . (len p) & f . 0 = id X & ( for i being Element of NAT st i + 1 in dom p holds

for g, h being Function st g = f . i & h = p . (i + 1) holds

f . (i + 1) = h * g ) ) & ex f being ManySortedFunction of NAT st

( b_{2} = f . (len p) & f . 0 = id X & ( for i being Element of NAT st i + 1 in dom p holds

for g, h being Function st g = f . i & h = p . (i + 1) holds

f . (i + 1) = h * g ) ) holds

b_{1} = b_{2}

existence

ex b_{1} being Function ex f being ManySortedFunction of NAT st

( b_{1} = f . (len p) & f . 0 = id X & ( for i being Element of NAT st i + 1 in dom p holds

for g, h being Function st g = f . i & h = p . (i + 1) holds

f . (i + 1) = h * g ) );

end;
let p be Function-yielding FinSequence;

func compose (p,X) -> Function means :Def4: :: FUNCT_7:def 4

ex f being ManySortedFunction of NAT st

( it = f . (len p) & f . 0 = id X & ( for i being Element of NAT st i + 1 in dom p holds

for g, h being Function st g = f . i & h = p . (i + 1) holds

f . (i + 1) = h * g ) );

uniqueness ex f being ManySortedFunction of NAT st

( it = f . (len p) & f . 0 = id X & ( for i being Element of NAT st i + 1 in dom p holds

for g, h being Function st g = f . i & h = p . (i + 1) holds

f . (i + 1) = h * g ) );

for b

( b

for g, h being Function st g = f . i & h = p . (i + 1) holds

f . (i + 1) = h * g ) ) & ex f being ManySortedFunction of NAT st

( b

for g, h being Function st g = f . i & h = p . (i + 1) holds

f . (i + 1) = h * g ) ) holds

b

proof end;

correctness existence

ex b

( b

for g, h being Function st g = f . i & h = p . (i + 1) holds

f . (i + 1) = h * g ) );

proof end;

:: deftheorem Def4 defines compose FUNCT_7:def 4 :

for X being set

for p being Function-yielding FinSequence

for b_{3} being Function holds

( b_{3} = compose (p,X) iff ex f being ManySortedFunction of NAT st

( b_{3} = f . (len p) & f . 0 = id X & ( for i being Element of NAT st i + 1 in dom p holds

for g, h being Function st g = f . i & h = p . (i + 1) holds

f . (i + 1) = h * g ) ) );

for X being set

for p being Function-yielding FinSequence

for b

( b

( b

for g, h being Function st g = f . i & h = p . (i + 1) holds

f . (i + 1) = h * g ) ) );

definition

let p be Function-yielding FinSequence;

let x be set ;

ex b_{1} being FinSequence st

( len b_{1} = (len p) + 1 & b_{1} . 1 = x & ( for i being Element of NAT

for f being Function st i in dom p & f = p . i holds

b_{1} . (i + 1) = f . (b_{1} . i) ) )

uniqueness

for b_{1}, b_{2} being FinSequence st len b_{1} = (len p) + 1 & b_{1} . 1 = x & ( for i being Element of NAT

for f being Function st i in dom p & f = p . i holds

b_{1} . (i + 1) = f . (b_{1} . i) ) & len b_{2} = (len p) + 1 & b_{2} . 1 = x & ( for i being Element of NAT

for f being Function st i in dom p & f = p . i holds

b_{2} . (i + 1) = f . (b_{2} . i) ) holds

b_{1} = b_{2};

end;
let x be set ;

func apply (p,x) -> FinSequence means :Def5: :: FUNCT_7:def 5

( len it = (len p) + 1 & it . 1 = x & ( for i being Element of NAT

for f being Function st i in dom p & f = p . i holds

it . (i + 1) = f . (it . i) ) );

existence ( len it = (len p) + 1 & it . 1 = x & ( for i being Element of NAT

for f being Function st i in dom p & f = p . i holds

it . (i + 1) = f . (it . i) ) );

ex b

( len b

for f being Function st i in dom p & f = p . i holds

b

proof end;

correctness uniqueness

for b

for f being Function st i in dom p & f = p . i holds

b

for f being Function st i in dom p & f = p . i holds

b

b

proof end;

:: deftheorem Def5 defines apply FUNCT_7:def 5 :

for p being Function-yielding FinSequence

for x being set

for b_{3} being FinSequence holds

( b_{3} = apply (p,x) iff ( len b_{3} = (len p) + 1 & b_{3} . 1 = x & ( for i being Element of NAT

for f being Function st i in dom p & f = p . i holds

b_{3} . (i + 1) = f . (b_{3} . i) ) ) );

for p being Function-yielding FinSequence

for x being set

for b

( b

for f being Function st i in dom p & f = p . i holds

b

theorem Th41: :: FUNCT_7:41

for X being set

for p being Function-yielding FinSequence

for f being Function holds compose ((p ^ <*f*>),X) = f * (compose (p,X))

for p being Function-yielding FinSequence

for f being Function holds compose ((p ^ <*f*>),X) = f * (compose (p,X))

proof end;

theorem Th42: :: FUNCT_7:42

for x being set

for p being Function-yielding FinSequence

for f being Function holds apply ((p ^ <*f*>),x) = (apply (p,x)) ^ <*(f . ((apply (p,x)) . ((len p) + 1)))*>

for p being Function-yielding FinSequence

for f being Function holds apply ((p ^ <*f*>),x) = (apply (p,x)) ^ <*(f . ((apply (p,x)) . ((len p) + 1)))*>

proof end;

theorem :: FUNCT_7:43

for X being set

for p being Function-yielding FinSequence

for f being Function holds compose ((<*f*> ^ p),X) = (compose (p,(f .: X))) * (f | X)

for p being Function-yielding FinSequence

for f being Function holds compose ((<*f*> ^ p),X) = (compose (p,(f .: X))) * (f | X)

proof end;

theorem :: FUNCT_7:44

for x being set

for p being Function-yielding FinSequence

for f being Function holds apply ((<*f*> ^ p),x) = <*x*> ^ (apply (p,(f . x)))

for p being Function-yielding FinSequence

for f being Function holds apply ((<*f*> ^ p),x) = <*x*> ^ (apply (p,(f . x)))

proof end;

theorem :: FUNCT_7:48

for X, Y being set

for p, q being Function-yielding FinSequence st rng (compose (p,X)) c= Y holds

compose ((p ^ q),X) = (compose (q,Y)) * (compose (p,X))

for p, q being Function-yielding FinSequence st rng (compose (p,X)) c= Y holds

compose ((p ^ q),X) = (compose (q,Y)) * (compose (p,X))

proof end;

theorem Th49: :: FUNCT_7:49

for x being set

for p, q being Function-yielding FinSequence holds (apply ((p ^ q),x)) . ((len (p ^ q)) + 1) = (apply (q,((apply (p,x)) . ((len p) + 1)))) . ((len q) + 1)

for p, q being Function-yielding FinSequence holds (apply ((p ^ q),x)) . ((len (p ^ q)) + 1) = (apply (q,((apply (p,x)) . ((len p) + 1)))) . ((len q) + 1)

proof end;

theorem :: FUNCT_7:50

for x being set

for p, q being Function-yielding FinSequence holds apply ((p ^ q),x) = (apply (p,x)) $^ (apply (q,((apply (p,x)) . ((len p) + 1))))

for p, q being Function-yielding FinSequence holds apply ((p ^ q),x) = (apply (p,x)) $^ (apply (q,((apply (p,x)) . ((len p) + 1))))

proof end;

theorem :: FUNCT_7:52

for X being set

for f, g being Function st ( dom f c= X or dom (g * f) c= X ) holds

compose (<*f,g*>,X) = g * f

for f, g being Function st ( dom f c= X or dom (g * f) c= X ) holds

compose (<*f,g*>,X) = g * f

proof end;

theorem :: FUNCT_7:55

for X being set

for f, g, h being Function st ( dom f c= X or dom (g * f) c= X or dom ((h * g) * f) c= X ) holds

compose (<*f,g,h*>,X) = (h * g) * f

for f, g, h being Function st ( dom f c= X or dom (g * f) c= X or dom ((h * g) * f) c= X ) holds

compose (<*f,g,h*>,X) = (h * g) * f

proof end;

theorem :: FUNCT_7:56

for x being set

for f, g, h being Function holds apply (<*f,g,h*>,x) = <*x*> ^ <*(f . x),(g . (f . x)),(h . (g . (f . x)))*>

for f, g, h being Function holds apply (<*f,g,h*>,x) = <*x*> ^ <*(f . x),(g . (f . x)),(h . (g . (f . x)))*>

proof end;

definition

let F be FinSequence;

consistency

for b_{1} being set holds verum;

existence

( ( for b_{1} being set holds verum ) & ( F is empty implies ex b_{1} being set st b_{1} is empty ) & ( not F is empty implies ex b_{1} being set st b_{1} = proj1 (F . 1) ) );

uniqueness

for b_{1}, b_{2} being set holds

( ( F is empty & b_{1} is empty & b_{2} is empty implies b_{1} = b_{2} ) & ( not F is empty & b_{1} = proj1 (F . 1) & b_{2} = proj1 (F . 1) implies b_{1} = b_{2} ) );

;

consistency

for b_{1} being set holds verum;

existence

( ( for b_{1} being set holds verum ) & ( F is empty implies ex b_{1} being set st b_{1} is empty ) & ( not F is empty implies ex b_{1} being set st b_{1} = proj2 (F . (len F)) ) );

uniqueness

for b_{1}, b_{2} being set holds

( ( F is empty & b_{1} is empty & b_{2} is empty implies b_{1} = b_{2} ) & ( not F is empty & b_{1} = proj2 (F . (len F)) & b_{2} = proj2 (F . (len F)) implies b_{1} = b_{2} ) );

;

end;
func firstdom F -> set means :Def6: :: FUNCT_7:def 6

it is empty if F is empty

otherwise it = proj1 (F . 1);

correctness it is empty if F is empty

otherwise it = proj1 (F . 1);

consistency

for b

existence

( ( for b

uniqueness

for b

( ( F is empty & b

;

func lastrng F -> set means :Def7: :: FUNCT_7:def 7

it is empty if F is empty

otherwise it = proj2 (F . (len F));

correctness it is empty if F is empty

otherwise it = proj2 (F . (len F));

consistency

for b

existence

( ( for b

uniqueness

for b

( ( F is empty & b

;

:: deftheorem Def6 defines firstdom FUNCT_7:def 6 :

for F being FinSequence

for b_{2} being set holds

( ( F is empty implies ( b_{2} = firstdom F iff b_{2} is empty ) ) & ( not F is empty implies ( b_{2} = firstdom F iff b_{2} = proj1 (F . 1) ) ) );

for F being FinSequence

for b

( ( F is empty implies ( b

:: deftheorem Def7 defines lastrng FUNCT_7:def 7 :

for F being FinSequence

for b_{2} being set holds

( ( F is empty implies ( b_{2} = lastrng F iff b_{2} is empty ) ) & ( not F is empty implies ( b_{2} = lastrng F iff b_{2} = proj2 (F . (len F)) ) ) );

for F being FinSequence

for b

( ( F is empty implies ( b

theorem Th58: :: FUNCT_7:58

for f being Function

for p being FinSequence holds

( firstdom (<*f*> ^ p) = dom f & lastrng (p ^ <*f*>) = rng f )

for p being FinSequence holds

( firstdom (<*f*> ^ p) = dom f & lastrng (p ^ <*f*>) = rng f )

proof end;

theorem Th59: :: FUNCT_7:59

for X being set

for p being Function-yielding FinSequence st p <> {} holds

rng (compose (p,X)) c= lastrng p

for p being Function-yielding FinSequence st p <> {} holds

rng (compose (p,X)) c= lastrng p

proof end;

:: deftheorem Def8 defines FuncSeq-like FUNCT_7:def 8 :

for IT being FinSequence holds

( IT is FuncSeq-like iff ex p being FinSequence st

( len p = (len IT) + 1 & ( for i being Element of NAT st i in dom IT holds

IT . i in Funcs ((p . i),(p . (i + 1))) ) ) );

for IT being FinSequence holds

( IT is FuncSeq-like iff ex p being FinSequence st

( len p = (len IT) + 1 & ( for i being Element of NAT st i in dom IT holds

IT . i in Funcs ((p . i),(p . (i + 1))) ) ) );

registration

coherence

for b_{1} being FinSequence st b_{1} is FuncSeq-like holds

b_{1} is Function-yielding

end;
for b

b

proof end;

registration
end;

registration
end;

registration

ex b_{1} being FinSequence st

( b_{1} is FuncSeq-like & not b_{1} is empty & b_{1} is non-empty )
end;

cluster non empty Relation-like non-empty NAT -defined Function-like finite FinSequence-like FinSubsequence-like FuncSeq-like for set ;

existence ex b

( b

proof end;

theorem :: FUNCT_7:63

for p being FuncSequence

for f being Function st rng f c= firstdom p holds

<*f*> ^ p is FuncSequence

for f being Function st rng f c= firstdom p holds

<*f*> ^ p is FuncSequence

proof end;

theorem :: FUNCT_7:65

for x, X being set

for p being FuncSequence st x in firstdom p & x in X holds

(apply (p,x)) . ((len p) + 1) = (compose (p,X)) . x

for p being FuncSequence st x in firstdom p & x in X holds

(apply (p,x)) . ((len p) + 1) = (compose (p,X)) . x

proof end;

definition

let X, Y be set ;

assume X1: ( Y is empty implies X is empty ) ;

ex b_{1} being FuncSequence st

( firstdom b_{1} = X & lastrng b_{1} c= Y )

end;
assume X1: ( Y is empty implies X is empty ) ;

mode FuncSequence of X,Y -> FuncSequence means :Def9: :: FUNCT_7:def 9

( firstdom it = X & lastrng it c= Y );

existence ( firstdom it = X & lastrng it c= Y );

ex b

( firstdom b

proof end;

:: deftheorem Def9 defines FuncSequence FUNCT_7:def 9 :

for X, Y being set st ( Y is empty implies X is empty ) holds

for b_{3} being FuncSequence holds

( b_{3} is FuncSequence of X,Y iff ( firstdom b_{3} = X & lastrng b_{3} c= Y ) );

for X, Y being set st ( Y is empty implies X is empty ) holds

for b

( b

definition

let Y be non empty set ;

let X be set ;

let F be FuncSequence of X,Y;

:: original: compose

redefine func compose (F,X) -> Function of X,Y;

coherence

compose (F,X) is Function of X,Y

end;
let X be set ;

let F be FuncSequence of X,Y;

:: original: compose

redefine func compose (F,X) -> Function of X,Y;

coherence

compose (F,X) is Function of X,Y

proof end;

definition

let q be non empty non-empty FinSequence;

ex b_{1} being FinSequence st

( (len b_{1}) + 1 = len q & ( for i being Element of NAT st i in dom b_{1} holds

b_{1} . i in Funcs ((q . i),(q . (i + 1))) ) )

end;
mode FuncSequence of q -> FinSequence means :Def10: :: FUNCT_7:def 10

( (len it) + 1 = len q & ( for i being Element of NAT st i in dom it holds

it . i in Funcs ((q . i),(q . (i + 1))) ) );

existence ( (len it) + 1 = len q & ( for i being Element of NAT st i in dom it holds

it . i in Funcs ((q . i),(q . (i + 1))) ) );

ex b

( (len b

b

proof end;

:: deftheorem Def10 defines FuncSequence FUNCT_7:def 10 :

for q being non empty non-empty FinSequence

for b_{2} being FinSequence holds

( b_{2} is FuncSequence of q iff ( (len b_{2}) + 1 = len q & ( for i being Element of NAT st i in dom b_{2} holds

b_{2} . i in Funcs ((q . i),(q . (i + 1))) ) ) );

for q being non empty non-empty FinSequence

for b

( b

b

registration

let q be non empty non-empty FinSequence;

coherence

for b_{1} being FuncSequence of q holds

( b_{1} is FuncSeq-like & b_{1} is non-empty )

end;
coherence

for b

( b

proof end;

theorem Th66: :: FUNCT_7:66

for q being non empty non-empty FinSequence

for p being FuncSequence of q st p <> {} holds

( firstdom p = q . 1 & lastrng p c= q . (len q) )

for p being FuncSequence of q st p <> {} holds

( firstdom p = q . 1 & lastrng p c= q . (len q) )

proof end;

theorem :: FUNCT_7:67

for q being non empty non-empty FinSequence

for p being FuncSequence of q holds

( dom (compose (p,(q . 1))) = q . 1 & rng (compose (p,(q . 1))) c= q . (len q) )

for p being FuncSequence of q holds

( dom (compose (p,(q . 1))) = q . 1 & rng (compose (p,(q . 1))) c= q . (len q) )

proof end;

:: Moved from FUNCT_4

registration

let X be set ;

let f be Function of NAT,(bool [:X,X:]);

let n be Nat;

coherence

f . n is Relation-like

end;
let f be Function of NAT,(bool [:X,X:]);

let n be Nat;

coherence

f . n is Relation-like

proof end;

Lm1: for X being set

for f being Function of X,X holds rng f c= dom f

proof end;

Lm2: for f being Relation

for n being Element of NAT

for p1, p2 being Function of NAT,(bool [:(field f),(field f):]) st p1 . 0 = id (field f) & ( for k being Nat holds p1 . (k + 1) = f * (p1 . k) ) & p2 . 0 = id (field f) & ( for k being Nat holds p2 . (k + 1) = f * (p2 . k) ) holds

p1 = p2

proof end;

definition

let f be Relation;

let n be Nat;

ex b_{1} being Relation ex p being Function of NAT,(bool [:(field f),(field f):]) st

( b_{1} = p . n & p . 0 = id (field f) & ( for k being Nat holds p . (k + 1) = f * (p . k) ) )

for b_{1}, b_{2} being Relation st ex p being Function of NAT,(bool [:(field f),(field f):]) st

( b_{1} = p . n & p . 0 = id (field f) & ( for k being Nat holds p . (k + 1) = f * (p . k) ) ) & ex p being Function of NAT,(bool [:(field f),(field f):]) st

( b_{2} = p . n & p . 0 = id (field f) & ( for k being Nat holds p . (k + 1) = f * (p . k) ) ) holds

b_{1} = b_{2}
by Lm2;

end;
let n be Nat;

func iter (f,n) -> Relation means :Def11: :: FUNCT_7:def 11

ex p being Function of NAT,(bool [:(field f),(field f):]) st

( it = p . n & p . 0 = id (field f) & ( for k being Nat holds p . (k + 1) = f * (p . k) ) );

existence ex p being Function of NAT,(bool [:(field f),(field f):]) st

( it = p . n & p . 0 = id (field f) & ( for k being Nat holds p . (k + 1) = f * (p . k) ) );

ex b

( b

proof end;

uniqueness for b

( b

( b

b

:: deftheorem Def11 defines iter FUNCT_7:def 11 :

for f being Relation

for n being Nat

for b_{3} being Relation holds

( b_{3} = iter (f,n) iff ex p being Function of NAT,(bool [:(field f),(field f):]) st

( b_{3} = p . n & p . 0 = id (field f) & ( for k being Nat holds p . (k + 1) = f * (p . k) ) ) );

for f being Relation

for n being Nat

for b

( b

( b

Lm3: for R being Relation holds

( (id (field R)) * R = R & R * (id (field R)) = R )

proof end;

Lm4: for R being Relation st rng R c= dom R holds

iter (R,0) = id (dom R)

proof end;

theorem Th72: :: FUNCT_7:72

for n being Element of NAT

for R being Relation holds

( dom (iter (R,n)) c= field R & rng (iter (R,n)) c= field R )

for R being Relation holds

( dom (iter (R,n)) c= field R & rng (iter (R,n)) c= field R )

proof end;

theorem :: FUNCT_7:73

for n being Element of NAT

for R being Relation st n <> 0 holds

( dom (iter (R,n)) c= dom R & rng (iter (R,n)) c= rng R )

for R being Relation st n <> 0 holds

( dom (iter (R,n)) c= dom R & rng (iter (R,n)) c= rng R )

proof end;

theorem Th74: :: FUNCT_7:74

for R being Relation

for n being Nat st rng R c= dom R holds

( dom (iter (R,n)) = dom R & rng (iter (R,n)) c= dom R )

for n being Nat st rng R c= dom R holds

( dom (iter (R,n)) = dom R & rng (iter (R,n)) c= dom R )

proof end;

theorem Th77: :: FUNCT_7:77

for m, n being Element of NAT

for R being Relation holds (iter (R,m)) * (iter (R,n)) = iter (R,(n + m))

for R being Relation holds (iter (R,m)) * (iter (R,n)) = iter (R,(n + m))

proof end;

Lm5: for m, k being Element of NAT

for R being Relation st iter ((iter (R,m)),k) = iter (R,(m * k)) holds

iter ((iter (R,m)),(k + 1)) = iter (R,(m * (k + 1)))

proof end;

theorem :: FUNCT_7:78

for n, m being Element of NAT

for R being Relation st n <> 0 holds

iter ((iter (R,m)),n) = iter (R,(m * n))

for R being Relation st n <> 0 holds

iter ((iter (R,m)),n) = iter (R,(m * n))

proof end;

theorem Th79: :: FUNCT_7:79

for m, n being Element of NAT

for R being Relation st rng R c= dom R holds

iter ((iter (R,m)),n) = iter (R,(m * n))

for R being Relation st rng R c= dom R holds

iter ((iter (R,m)),n) = iter (R,(m * n))

proof end;

theorem :: FUNCT_7:85

for X being set

for m, n being Element of NAT

for f being Function of X,X holds iter ((iter (f,m)),n) = iter (f,(m * n))

for m, n being Element of NAT

for f being Function of X,X holds iter ((iter (f,m)),n) = iter (f,(m * n))

proof end;

theorem :: FUNCT_7:86

for X being set

for n being Element of NAT

for f being PartFunc of X,X holds iter (f,n) is PartFunc of X,X

for n being Element of NAT

for f being PartFunc of X,X holds iter (f,n) is PartFunc of X,X

proof end;

theorem :: FUNCT_7:87

for a, X being set

for f being Function

for n being Element of NAT st n <> 0 & a in X & f = X --> a holds

iter (f,n) = f

for f being Function

for n being Element of NAT st n <> 0 & a in X & f = X --> a holds

iter (f,n) = f

proof end;

begin

:: from SCMFSA6A, 2006.03.14, A.T.

theorem :: FUNCT_7:93

for f, g being Function

for a, b, A being set st f | A = g | A holds

(f +* (a,b)) | A = (g +* (a,b)) | A

for a, b, A being set st f | A = g | A holds

(f +* (a,b)) | A = (g +* (a,b)) | A

proof end;

:: from YELLOW14, 2006.03.14, A.T.

:: from SCMFSA6A, 2006.03.14, A.T.

:: from SCMFSA8C, 2006.03.15

theorem :: FUNCT_7:98

for i being Nat

for D being non empty set

for w being FinSequence of D

for r being Element of D st i in dom w holds

w +* (i,r) = ((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)

for D being non empty set

for w being FinSequence of D

for r being Element of D st i in dom w holds

w +* (i,r) = ((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)

proof end;

definition

let F be Function;

let x, y be set ;

coherence

( ( x in dom F & y in dom F implies (F +* (x,(F . y))) +* (y,(F . x)) is set ) & ( ( not x in dom F or not y in dom F ) implies F is set ) );

consistency

for b_{1} being set holds verum;

;

end;
let x, y be set ;

func Swap (F,x,y) -> set equals :Def12: :: FUNCT_7:def 12

(F +* (x,(F . y))) +* (y,(F . x)) if ( x in dom F & y in dom F )

otherwise F;

correctness (F +* (x,(F . y))) +* (y,(F . x)) if ( x in dom F & y in dom F )

otherwise F;

coherence

( ( x in dom F & y in dom F implies (F +* (x,(F . y))) +* (y,(F . x)) is set ) & ( ( not x in dom F or not y in dom F ) implies F is set ) );

consistency

for b

;

:: deftheorem Def12 defines Swap FUNCT_7:def 12 :

for F being Function

for x, y being set holds

( ( x in dom F & y in dom F implies Swap (F,x,y) = (F +* (x,(F . y))) +* (y,(F . x)) ) & ( ( not x in dom F or not y in dom F ) implies Swap (F,x,y) = F ) );

for F being Function

for x, y being set holds

( ( x in dom F & y in dom F implies Swap (F,x,y) = (F +* (x,(F . y))) +* (y,(F . x)) ) & ( ( not x in dom F or not y in dom F ) implies Swap (F,x,y) = F ) );

registration

let F be Function;

let x, y be set ;

coherence

( Swap (F,x,y) is Relation-like & Swap (F,x,y) is Function-like )

end;
let x, y be set ;

coherence

( Swap (F,x,y) is Relation-like & Swap (F,x,y) is Function-like )

proof end;

:: from SCMFSA_7, 2007.07.22, A.T.

:: from SCMFSA6A, 2007.07.23, A.T.

theorem :: FUNCT_7:104

for f, g, h being Function

for A being set st f,g equal_outside A holds

f +* h,g +* h equal_outside A

for A being set st f,g equal_outside A holds

f +* h,g +* h equal_outside A

proof end;

theorem :: FUNCT_7:105

for f, g, h being Function

for A being set st f,g equal_outside A holds

h +* f,h +* g equal_outside A

for A being set st f,g equal_outside A holds

h +* f,h +* g equal_outside A

proof end;

:: from SF_MASTR, 2007.07.25, A.T.

theorem Th107: :: FUNCT_7:107

for x, y, a being set

for f being Function st f . x = f . y holds

f . a = (f * ((id (dom f)) +* (x,y))) . a

for f being Function st f . x = f . y holds

f . a = (f * ((id (dom f)) +* (x,y))) . a

proof end;

theorem :: FUNCT_7:108

for x, y being set

for f being Function st ( x in dom f implies ( y in dom f & f . x = f . y ) ) holds

f = f * ((id (dom f)) +* (x,y))

for f being Function st ( x in dom f implies ( y in dom f & f . x = f . y ) ) holds

f = f * ((id (dom f)) +* (x,y))

proof end;

:: from SCMFSA8C, 2007.07.26, A.T.

:: from SFMASTR3, 2007.07.26, A.T.

theorem Th110: :: FUNCT_7:110

for X being set

for p being Permutation of X

for x, y being Element of X holds (p +* (x,(p . y))) +* (y,(p . x)) is Permutation of X

for p being Permutation of X

for x, y being Element of X holds (p +* (x,(p . y))) +* (y,(p . x)) is Permutation of X

proof end;

theorem :: FUNCT_7:111

for f being Function

for x, y being set st x in dom f & y in dom f holds

ex p being Permutation of (dom f) st (f +* (x,(f . y))) +* (y,(f . x)) = f * p

for x, y being set st x in dom f & y in dom f holds

ex p being Permutation of (dom f) st (f +* (x,(f . y))) +* (y,(f . x)) = f * p

proof end;

:: from SCMISORT, 2007.07.26, A.T.

:: from SCMBISORT, 2007.07.26, A.T.

theorem :: FUNCT_7:113

for f, g being FinSequence of INT

for m, n being Element of NAT st 1 <= n & n <= len f & 1 <= m & m <= len f & g = (f +* (m,(f /. n))) +* (n,(f /. m)) holds

( f . m = g . n & f . n = g . m & ( for k being set st k <> m & k <> n & k in dom f holds

f . k = g . k ) & f,g are_fiberwise_equipotent )

for m, n being Element of NAT st 1 <= n & n <= len f & 1 <= m & m <= len f & g = (f +* (m,(f /. n))) +* (n,(f /. m)) holds

( f . m = g . n & f . n = g . m & ( for k being set st k <> m & k <> n & k in dom f holds

f . k = g . k ) & f,g are_fiberwise_equipotent )

proof end;

:: from SCMFSA10, 2007.07.27, A.T.

theorem :: FUNCT_7:114

for f being Function

for a, A, b, B, c, C being set st a <> b & a <> c holds

(((f +* (a .--> A)) +* (b .--> B)) +* (c .--> C)) . a = A

for a, A, b, B, c, C being set st a <> b & a <> c holds

(((f +* (a .--> A)) +* (b .--> B)) +* (c .--> C)) . a = A

proof end;

:: comp TOPALG_3:1, 2008.01.18, A.T.

:: missing, 2008.03.23, A.T.

theorem Th116: :: FUNCT_7:116

for A being set

for f being Function

for x, y being set st rng f c= A holds

f +~ (x,y) = ((id A) +* (x,y)) * f

for f being Function

for x, y being set st rng f c= A holds

f +~ (x,y) = ((id A) +* (x,y)) * f

proof end;

:: deftheorem defines followed_by FUNCT_7:def 13 :

for a, b being set holds a followed_by b = (NAT --> b) +* (0,a);

for a, b being set holds a followed_by b = (NAT --> b) +* (0,a);

registration

let a, b be set ;

coherence

( a followed_by b is Function-like & a followed_by b is Relation-like ) ;

end;
coherence

( a followed_by b is Function-like & a followed_by b is Relation-like ) ;

definition

let X be non empty set ;

let a, b be Element of X;

:: original: followed_by

redefine func a followed_by b -> sequence of X;

coherence

a followed_by b is sequence of X

end;
let a, b be Element of X;

:: original: followed_by

redefine func a followed_by b -> sequence of X;

coherence

a followed_by b is sequence of X

proof end;

:: from DYNKIN, 2008.09.24, A.T.

:: deftheorem defines followed_by FUNCT_7:def 14 :

for a, b, c being set holds (a,b) followed_by c = (NAT --> c) +* ((0,1) --> (a,b));

for a, b, c being set holds (a,b) followed_by c = (NAT --> c) +* ((0,1) --> (a,b));

registration

let a, b, c be set ;

coherence

( (a,b) followed_by c is Function-like & (a,b) followed_by c is Relation-like ) ;

end;
coherence

( (a,b) followed_by c is Function-like & (a,b) followed_by c is Relation-like ) ;

definition

let X be non empty set ;

let a, b, c be Element of X;

:: original: followed_by

redefine func (a,b) followed_by c -> sequence of X;

coherence

(a,b) followed_by c is sequence of X

end;
let a, b, c be Element of X;

:: original: followed_by

redefine func (a,b) followed_by c -> sequence of X;

coherence

(a,b) followed_by c is sequence of X

proof end;

:: from POLYNOM1, 2008.12.15, A.T.

definition

let A, B be set ;

let f be Function of A,B;

let x be set ;

let y be Element of B;

:: original: +*

redefine func f +* (x,y) -> Function of A,B;

coherence

f +* (x,y) is Function of A,B

end;
let f be Function of A,B;

let x be set ;

let y be Element of B;

:: original: +*

redefine func f +* (x,y) -> Function of A,B;

coherence

f +* (x,y) is Function of A,B

proof end;

:: missing, 2008.12.14, A.T.

theorem :: FUNCT_7:128

for A, B being non empty set

for f being Function of A,B

for x being Element of A

for y being set holds (f +* (x,y)) . x = y

for f being Function of A,B

for x being Element of A

for y being set holds (f +* (x,y)) . x = y

proof end;

theorem :: FUNCT_7:129

for A, B being non empty set

for f, g being Function of A,B

for x being Element of A st ( for y being Element of A st f . y <> g . y holds

y = x ) holds

f = g +* (x,(f . x))

for f, g being Function of A,B

for x being Element of A st ( for y being Element of A st f . y <> g . y holds

y = x ) holds

f = g +* (x,(f . x))

proof end;

theorem Th130: :: FUNCT_7:130

for A being set

for f being Function

for g being b_{1} -defined Function holds f,f +* g equal_outside A

for f being Function

for g being b

proof end;

theorem :: FUNCT_7:132

for A being set

for f, g being b_{1} -defined Function

for h being Function holds h +* f,h +* g equal_outside A

for f, g being b

for h being Function holds h +* f,h +* g equal_outside A

proof end;

theorem Th134: :: FUNCT_7:134

for A, B being set

for f, g being Function st dom f = dom g & dom f c= A \/ B & f | B = g | B holds

f,g equal_outside A

for f, g being Function st dom f = dom g & dom f c= A \/ B & f | B = g | B holds

f,g equal_outside A

proof end;

theorem Th135: :: FUNCT_7:135

for B, A being set

for f, g being Function st dom f = dom g & B c= dom f & A misses B & f,g equal_outside A holds

f | B = g | B

for f, g being Function st dom f = dom g & B c= dom f & A misses B & f,g equal_outside A holds

f | B = g | B

proof end;

theorem :: FUNCT_7:136

for I, A, B being set

for X, Y being ManySortedSet of I st I c= A \/ B & X | B = Y | B holds

X,Y equal_outside A

for X, Y being ManySortedSet of I st I c= A \/ B & X | B = Y | B holds

X,Y equal_outside A

proof end;

theorem :: FUNCT_7:137

for B, I, A being set

for X, Y being ManySortedSet of I st B c= I & A misses B & X,Y equal_outside A holds

X | B = Y | B

for X, Y being ManySortedSet of I st B c= I & A misses B & X,Y equal_outside A holds

X | B = Y | B

proof end;

registration

let V be non empty set ;

let f be V -valued Function;

let x be set ;

let y be Element of V;

coherence

f +* (x,y) is V -valued

end;
let f be V -valued Function;

let x be set ;

let y be Element of V;

coherence

f +* (x,y) is V -valued

proof end;

theorem :: FUNCT_7:139

for I being non empty set

for X being ManySortedSet of I

for l1, l2 being Element of I

for i1, i2 being set holds X +* ((l1,l2) --> (i1,i2)) = (X +* (l1,i1)) +* (l2,i2)

for X being ManySortedSet of I

for l1, l2 being Element of I

for i1, i2 being set holds X +* ((l1,l2) --> (i1,i2)) = (X +* (l1,i1)) +* (l2,i2)

proof end;