:: Miscellaneous Facts about Functions
:: by Grzegorz Bancerek and Andrzej Trybulec
::
:: Received January 12, 1996
:: Copyright (c) 1996-2011 Association of Mizar Users

begin

theorem :: FUNCT_7:1

for f being Function
for X being set st rng f c= X holds
(id X) * f = f

proof end;

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

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

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)

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)

proof end;

theorem Th6: :: FUNCT_7:6

for f being Function
for a being set st a in dom f holds
f | {a} = a .--> (f . a)

proof end;

registration

let x, y be set ;
cluster x .--> y -> non empty ;
coherence
not x .--> y is empty ;

end;

registration

let x, y, a, b be set ;
cluster (x,y) --> (a,b) -> non empty ;
coherence
not (x,y) --> (a,b) is empty ;

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}

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}:]

proof end;

theorem :: FUNCT_7:9

canceled;

theorem Th10: :: FUNCT_7:10

for f, g, h being Function st rng h c= dom f holds
f * (g +* h) = (f * g) +* (f * h)

proof end;

theorem Th11: :: FUNCT_7:11

for f, g, h being Function holds (g +* h) * f = (g * f) +* (h * f)

proof end;

theorem :: FUNCT_7:12

for f, g, h being Function st rng f misses dom g holds
(h +* g) * f = h * f

proof end;

theorem Th13: :: FUNCT_7:13

for A, B, y being set st A meets rng ((id B) +* (A --> y)) holds
y in A

proof end;

theorem :: FUNCT_7:14

for x, y, A being set st x <> y holds
not x in rng ((id A) +* (x .--> y))

proof end;

theorem :: FUNCT_7:15

for X, a being set
for f being Function st dom f = X \/ {a} holds
f = (f | X) +* (a .--> (f . a))

proof end;

theorem :: FUNCT_7:16

for f being Function
for X, y, z being set holds (f +* (X --> y)) +* (X --> z) = f +* (X --> z)

proof end;

theorem :: FUNCT_7:17

canceled;

theorem :: FUNCT_7:18

INT <> INT *

proof end;

theorem :: FUNCT_7:19

{} * = {{}}

proof end;

theorem Th20: :: FUNCT_7:20

for x, A being set holds
( <*x*> in A * iff x in A )

proof end;

theorem :: FUNCT_7:21

for A, B being set st A * c= B * holds
A c= B

proof end;

theorem :: FUNCT_7:22

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

proof end;

theorem :: FUNCT_7:23

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

proof end;

theorem Th24: :: FUNCT_7:24

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 ) )

proof end;

registration

cluster non empty Relation-like non-empty Function-like Function-yielding finite FinSequence-like FinSubsequence-like set ;
existence
ex b₁ being FinSequence st
( b₁ is Function-yielding & not b₁ is empty & b₁ is non-empty )

proof end;

end;

registration

cluster empty Relation-like Function-like -> Function-yielding set ;
coherence
for b₁ being Function st b₁ is empty holds
b₁ is Function-yielding

proof end;

let f be Function;
cluster <*f*> -> Function-yielding ;
coherence
<*f*> is Function-yielding

proof end;

let g be Function;
cluster <*f,g*> -> Function-yielding ;
coherence
<*f,g*> is Function-yielding

proof end;

let h be Function;
cluster <*f,g,h*> -> Function-yielding ;
coherence
<*f,g,h*> is Function-yielding

proof end;

end;

registration

let n be Element of NAT ;
let f be Function;
cluster n |-> f -> Function-yielding ;
coherence
n |-> f is Function-yielding ;

end;

registration

let p, q be Function-yielding FinSequence;
cluster p ^ q -> Function-yielding ;
coherence
p ^ q is Function-yielding

proof end;

end;

theorem Th25: :: FUNCT_7:25

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

proof end;

begin

scheme :: FUNCT_7:sch 1
Kappa2D{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> non empty set , F₄( Element of F₁(), Element of F₂()) -> set } :

ex f being Function of [:F₁(),F₂():],F₃() st
for x being Element of F₁()
for y being Element of F₂() holds f . (x,y) = F₄(x,y)

provided

A1: for x being Element of F₁()
for y being Element of F₂() holds F₄(x,y) in F₃()

proof end;

scheme :: FUNCT_7:sch 2
FinMono{ F₁() -> set , F₂() -> non empty set , F₃( set ) -> set , F₄( set ) -> set } :

{ F₃(d) where d is Element of F₂() : F₄(d) in F₁() } is finite

provided

A1: F₁() is finite and
A2: for d1, d2 being Element of F₂() st F₄(d1) = F₄(d2) holds
d1 = d2

proof end;

scheme :: FUNCT_7:sch 3
CardMono{ F₁() -> set , F₂() -> non empty set , F₃( set ) -> set } :

F₁(), { d where d is Element of F₂() : F₃(d) in F₁() } are_equipotent

provided

A1: for x being set st x in F₁() holds
ex d being Element of F₂() st x = F₃(d) and
A2: for d1, d2 being Element of F₂() st F₃(d1) = F₃(d2) holds
d1 = d2

proof end;

scheme :: FUNCT_7:sch 4
CardMono9{ F₁() -> set , F₂() -> non empty set , F₃( set ) -> set } :

F₁(), { F₃(d) where d is Element of F₂() : d in F₁() } are_equipotent

provided

A1: F₁() c= F₂() and
A2: for d1, d2 being Element of F₂() st F₃(d1) = F₃(d2) holds
d1 = d2

proof end;

scheme :: FUNCT_7:sch 5
FuncSeqInd{ P₁[ set ] } :

for p being Function-yielding FinSequence holds P₁[p]

provided

A1: P₁[ {} ] and
A2: for p being Function-yielding FinSequence st P₁[p] holds
for f being Function holds P₁[p ^ <*f*>]

proof end;

begin

definition

let x, y be set ;
assume A1: x in y ;
func In (x,y) -> Element of y equals :Def1: :: FUNCT_7:def 1
x;
correctness
coherence
x is Element of y;
by A1;

end;

:: deftheorem Def1 defines In FUNCT_7:def 1 :
for x, y being set st x in y holds
In (x,y) = x;

theorem :: FUNCT_7:26

for x, A, B being set st x in A /\ B holds
In (x,A) = In (x,B)

proof end;

definition

let f, g be Function;
let A be set ;
pred f,g equal_outside A means :Def2: :: FUNCT_7:def 2
f | ((dom f) \ A) = g | ((dom g) \ A);

end;

:: 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) );

theorem Th27: :: FUNCT_7:27

for f being Function
for A being set holds f,f equal_outside A

proof end;

theorem Th28: :: FUNCT_7:28

for f, g being Function
for A being set st f,g equal_outside A holds
g,f equal_outside A

proof end;

theorem Th29: :: FUNCT_7:29

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

proof end;

theorem Th30: :: FUNCT_7:30

for f, g being Function
for A being set st f,g equal_outside A holds
(dom f) \ A = (dom g) \ A

proof end;

theorem Th31: :: FUNCT_7:31

for f, g being Function
for A being set st dom g c= A holds
f,f +* g equal_outside A

proof end;

definition

let f be Function;
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
coherence
( ( i in dom f implies f +* (i .--> x) is Function ) & ( not i in dom f implies f is Function ) );
consistency
for b₁ being Function holds verum;
;

end;

:: 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 ) );

theorem Th32: :: FUNCT_7:32

for f being Function
for d, i being set holds dom (f +* (i,d)) = dom f

proof end;

theorem Th33: :: FUNCT_7:33

for f being Function
for d, i being set st i in dom f holds
(f +* (i,d)) . i = d

proof end;

theorem Th34: :: FUNCT_7:34

for f being Function
for d, i, j being set st i <> j holds
(f +* (i,d)) . j = f . j

proof end;

theorem :: FUNCT_7:35

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)

proof end;

theorem :: FUNCT_7:36

for f being Function
for d, e, i being set holds (f +* (i,d)) +* (i,e) = f +* (i,e)

proof end;

theorem Th37: :: FUNCT_7:37

for f being Function
for i being set holds f +* (i,(f . i)) = f

proof end;

registration

let f be FinSequence;
let i, x be set ;
cluster f +* (i,x) -> FinSequence-like ;
coherence
f +* (i,x) is FinSequence-like

proof end;

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

proof end;

end;

theorem :: FUNCT_7:38

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

proof end;

theorem :: FUNCT_7:39

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

proof end;

theorem :: FUNCT_7:40

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

proof end;

begin

definition

let X be set ;
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
for b₁, b₂ being Function st ex f being ManySortedFunction of NAT st
( b₁ = 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₂ = 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₁ = b₂

proof end;

correctness
existence
ex b₁ being Function ex f being ManySortedFunction of NAT st
( b₁ = 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 ) );

proof end;

end;

:: deftheorem Def4 defines compose FUNCT_7:def 4 :
for X being set
for p being Function-yielding FinSequence
for b₃ being Function holds
( b₃ = compose (p,X) iff ex f being ManySortedFunction of NAT st
( b₃ = 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 ) ) );

definition

let p be Function-yielding FinSequence;
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
ex b₁ being FinSequence st
( len b₁ = (len p) + 1 & b₁ . 1 = x & ( for i being Element of NAT
for f being Function st i in dom p & f = p . i holds
b₁ . (i + 1) = f . (b₁ . i) ) )

proof end;

correctness
uniqueness
for b₁, b₂ being FinSequence st len b₁ = (len p) + 1 & b₁ . 1 = x & ( for i being Element of NAT
for f being Function st i in dom p & f = p . i holds
b₁ . (i + 1) = f . (b₁ . i) ) & len b₂ = (len p) + 1 & b₂ . 1 = x & ( for i being Element of NAT
for f being Function st i in dom p & f = p . i holds
b₂ . (i + 1) = f . (b₂ . i) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def5 defines apply FUNCT_7:def 5 :
for p being Function-yielding FinSequence
for x being set
for b₃ being FinSequence holds
( b₃ = apply (p,x) iff ( len b₃ = (len p) + 1 & b₃ . 1 = x & ( for i being Element of NAT
for f being Function st i in dom p & f = p . i holds
b₃ . (i + 1) = f . (b₃ . i) ) ) );

theorem Th41: :: FUNCT_7:41

for X being set holds compose ({},X) = id X

proof end;

theorem Th42: :: FUNCT_7:42

for x being set holds apply ({},x) = <*x*>

proof end;

theorem Th43: :: FUNCT_7:43

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

proof end;

theorem Th44: :: FUNCT_7:44

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)))*>

proof end;

theorem :: FUNCT_7:45

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)

proof end;

theorem :: FUNCT_7:46

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

proof end;

theorem Th47: :: FUNCT_7:47

for X being set
for f being Function holds compose (<*f*>,X) = f * (id X)

proof end;

theorem :: FUNCT_7:48

for X being set
for f being Function st dom f c= X holds
compose (<*f*>,X) = f

proof end;

theorem Th49: :: FUNCT_7:49

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

proof end;

theorem :: FUNCT_7:50

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))

proof end;

theorem Th51: :: FUNCT_7:51

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)

proof end;

theorem :: FUNCT_7:52

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))))

proof end;

theorem Th53: :: FUNCT_7:53

for X being set
for f, g being Function holds compose (<*f,g*>,X) = (g * f) * (id X)

proof end;

theorem :: FUNCT_7:54

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

proof end;

theorem Th55: :: FUNCT_7:55

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

proof end;

theorem Th56: :: FUNCT_7:56

for X being set
for f, g, h being Function holds compose (<*f,g,h*>,X) = ((h * g) * f) * (id X)

proof end;

theorem :: FUNCT_7:57

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

proof end;

theorem :: FUNCT_7:58

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)))*>

proof end;

definition

let F be FinSequence;
func firstdom F -> set means :Def6: :: FUNCT_7:def 6
it is empty if F is empty
otherwise it = proj1 (F . 1);
correctness
consistency
for b₁ being set holds verum;
existence
( ( for b₁ being set holds verum ) & ( F is empty implies ex b₁ being set st b₁ is empty ) & ( not F is empty implies ex b₁ being set st b₁ = proj1 (F . 1) ) );
uniqueness
for b₁, b₂ being set holds
( ( F is empty & b₁ is empty & b₂ is empty implies b₁ = b₂ ) & ( not F is empty & b₁ = proj1 (F . 1) & b₂ = proj1 (F . 1) implies b₁ = 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
consistency
for b₁ being set holds verum;
existence
( ( for b₁ being set holds verum ) & ( F is empty implies ex b₁ being set st b₁ is empty ) & ( not F is empty implies ex b₁ being set st b₁ = proj2 (F . (len F)) ) );
uniqueness
for b₁, b₂ being set holds
( ( F is empty & b₁ is empty & b₂ is empty implies b₁ = b₂ ) & ( not F is empty & b₁ = proj2 (F . (len F)) & b₂ = proj2 (F . (len F)) implies b₁ = b₂ ) );
;

end;

:: deftheorem Def6 defines firstdom FUNCT_7:def 6 :
for F being FinSequence
for b₂ being set holds
( ( F is empty implies ( b₂ = firstdom F iff b₂ is empty ) ) & ( not F is empty implies ( b₂ = firstdom F iff b₂ = proj1 (F . 1) ) ) );

:: deftheorem Def7 defines lastrng FUNCT_7:def 7 :
for F being FinSequence
for b₂ being set holds
( ( F is empty implies ( b₂ = lastrng F iff b₂ is empty ) ) & ( not F is empty implies ( b₂ = lastrng F iff b₂ = proj2 (F . (len F)) ) ) );

theorem Th59: :: FUNCT_7:59

( firstdom {} = {} & lastrng {} = {} ) by Def6, Def7;

theorem Th60: :: FUNCT_7:60

for f being Function
for p being FinSequence holds
( firstdom (<*f*> ^ p) = dom f & lastrng (p ^ <*f*>) = rng f )

proof end;

theorem Th61: :: FUNCT_7:61

for X being set
for p being Function-yielding FinSequence st p <> {} holds
rng (compose (p,X)) c= lastrng p

proof end;

definition

let IT be FinSequence;
attr IT is FuncSeq-like means :Def8: :: FUNCT_7:def 8
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))) ) );

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))) ) ) );

theorem Th62: :: FUNCT_7:62

for p, q being FinSequence st p ^ q is FuncSeq-like holds
( p is FuncSeq-like & q is FuncSeq-like )

proof end;

registration

cluster Relation-like Function-like FinSequence-like FuncSeq-like -> Function-yielding set ;
coherence
for b₁ being FinSequence st b₁ is FuncSeq-like holds
b₁ is Function-yielding

proof end;

end;

registration

cluster empty Relation-like Function-like FinSequence-like -> FuncSeq-like set ;
coherence
for b₁ being FinSequence st b₁ is empty holds
b₁ is FuncSeq-like

proof end;

end;

registration

let f be Function;
cluster <*f*> -> FuncSeq-like ;
coherence
<*f*> is FuncSeq-like

proof end;

end;

registration

cluster non empty Relation-like non-empty Function-like finite FinSequence-like FinSubsequence-like FuncSeq-like set ;
existence
ex b₁ being FinSequence st
( b₁ is FuncSeq-like & not b₁ is empty & b₁ is non-empty )

proof end;

end;

definition

mode FuncSequence is FuncSeq-like FinSequence;

end;

theorem Th63: :: FUNCT_7:63

for X being set
for p being FuncSequence st p <> {} holds
dom (compose (p,X)) = (firstdom p) /\ X

proof end;

theorem Th64: :: FUNCT_7:64

for p being FuncSequence holds dom (compose (p,(firstdom p))) = firstdom p

proof end;

theorem :: FUNCT_7:65

for p being FuncSequence
for f being Function st rng f c= firstdom p holds
<*f*> ^ p is FuncSequence

proof end;

theorem :: FUNCT_7:66

for p being FuncSequence
for f being Function st lastrng p c= dom f holds
p ^ <*f*> is FuncSequence

proof end;

theorem :: FUNCT_7:67

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

proof end;

definition

let X, Y be set ;
assume A1: ( 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
ex b₁ being FuncSequence st
( firstdom b₁ = X & lastrng b₁ c= Y )

proof end;

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₃ being FuncSequence holds
( b₃ is FuncSequence of X,Y iff ( firstdom b₃ = X & lastrng b₃ c= Y ) );

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

proof end;

end;

definition

let q be non empty non-empty FinSequence;
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
ex b₁ being FinSequence st
( (len b₁) + 1 = len q & ( for i being Element of NAT st i in dom b₁ holds
b₁ . i in Funcs ((q . i),(q . (i + 1))) ) )

proof end;

end;

:: deftheorem Def10 defines FuncSequence FUNCT_7:def 10 :
for q being non empty non-empty FinSequence
for b₂ being FinSequence holds
( b₂ is FuncSequence of q iff ( (len b₂) + 1 = len q & ( for i being Element of NAT st i in dom b₂ holds
b₂ . i in Funcs ((q . i),(q . (i + 1))) ) ) );

registration

let q be non empty non-empty FinSequence;
cluster -> non-empty FuncSeq-like FuncSequence of q;
coherence
for b₁ being FuncSequence of q holds
( b₁ is FuncSeq-like & b₁ is non-empty )

proof end;

end;

theorem Th68: :: FUNCT_7:68

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) )

proof end;

theorem :: FUNCT_7:69

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) )

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 Function
for n being Element of NAT
for p1, p2 being Function of NAT,(PFuncs ((field f),(field f))) st p1 . 0 = id (field f) & ( for k being Nat holds p1 . (k + 1) = (p1 . k) * f ) & p2 . 0 = id (field f) & ( for k being Nat holds p2 . (k + 1) = (p2 . k) * f ) holds
p1 = p2

proof end;

definition

let f be Function;
let n be Nat;
func iter (f,n) -> Function means :Def11: :: FUNCT_7:def 11
ex p being Function of NAT,(PFuncs ((field f),(field f))) st
( it = p . n & p . 0 = id (field f) & ( for k being Nat holds p . (k + 1) = (p . k) * f ) );
existence
ex b₁ being Function ex p being Function of NAT,(PFuncs ((field f),(field f))) st
( b₁ = p . n & p . 0 = id (field f) & ( for k being Nat holds p . (k + 1) = (p . k) * f ) )

proof end;

uniqueness
for b₁, b₂ being Function st ex p being Function of NAT,(PFuncs ((field f),(field f))) st
( b₁ = p . n & p . 0 = id (field f) & ( for k being Nat holds p . (k + 1) = (p . k) * f ) ) & ex p being Function of NAT,(PFuncs ((field f),(field f))) st
( b₂ = p . n & p . 0 = id (field f) & ( for k being Nat holds p . (k + 1) = (p . k) * f ) ) holds
b₁ = b₂ by Lm2;

end;

:: deftheorem Def11 defines iter FUNCT_7:def 11 :
for f being Function
for n being Nat
for b₃ being Function holds
( b₃ = iter (f,n) iff ex p being Function of NAT,(PFuncs ((field f),(field f))) st
( b₃ = p . n & p . 0 = id (field f) & ( for k being Nat holds p . (k + 1) = (p . k) * f ) ) );

Lm3: for f being Function holds
( (id (field f)) * f = f & f * (id (field f)) = f )

proof end;

theorem Th70: :: FUNCT_7:70

for f being Function holds iter (f,0) = id (field f)

proof end;

Lm4: for f being Function st rng f c= dom f holds
iter (f,0) = id (dom f)

proof end;

theorem Th71: :: FUNCT_7:71

for f being Function
for n being Nat holds iter (f,(n + 1)) = (iter (f,n)) * f

proof end;

theorem Th72: :: FUNCT_7:72

for f being Function holds iter (f,1) = f

proof end;

theorem Th73: :: FUNCT_7:73

for f being Function
for n being Nat holds iter (f,(n + 1)) = f * (iter (f,n))

proof end;

theorem Th74: :: FUNCT_7:74

for f being Function
for n being Element of NAT holds
( dom (iter (f,n)) c= field f & rng (iter (f,n)) c= field f )

proof end;

theorem :: FUNCT_7:75

for f being Function
for n being Element of NAT st n <> 0 holds
( dom (iter (f,n)) c= dom f & rng (iter (f,n)) c= rng f )

proof end;

theorem Th76: :: FUNCT_7:76

for f being Function
for n being Nat st rng f c= dom f holds
( dom (iter (f,n)) = dom f & rng (iter (f,n)) c= dom f )

proof end;

theorem Th77: :: FUNCT_7:77

for f being Function
for n being Element of NAT holds (iter (f,n)) * (id (field f)) = iter (f,n)

proof end;

theorem :: FUNCT_7:78

for f being Function
for n being Element of NAT holds (id (field f)) * (iter (f,n)) = iter (f,n)

proof end;

theorem Th79: :: FUNCT_7:79

for f being Function
for n, m being Element of NAT holds (iter (f,n)) * (iter (f,m)) = iter (f,(n + m))

proof end;

Lm5: for f being Function
for m, k being Element of NAT st iter ((iter (f,m)),k) = iter (f,(m * k)) holds
iter ((iter (f,m)),(k + 1)) = iter (f,(m * (k + 1)))

proof end;

theorem :: FUNCT_7:80

for f being Function
for n, m being Element of NAT st n <> 0 holds
iter ((iter (f,m)),n) = iter (f,(m * n))

proof end;

theorem Th81: :: FUNCT_7:81

for f being Function
for m, n being Element of NAT st rng f c= dom f holds
iter ((iter (f,m)),n) = iter (f,(m * n))

proof end;

theorem :: FUNCT_7:82

for n being Element of NAT holds iter ({},n) = {}

proof end;

theorem :: FUNCT_7:83

for X being set
for n being Element of NAT holds iter ((id X),n) = id X

proof end;

theorem :: FUNCT_7:84

for f being Function st rng f misses dom f holds
iter (f,2) = {}

proof end;

theorem :: FUNCT_7:85

for X being set
for n being Nat
for f being Function of X,X holds iter (f,n) is Function of X,X

proof end;

theorem :: FUNCT_7:86

for X being set
for f being Function of X,X holds iter (f,0) = id X

proof end;

theorem :: FUNCT_7:87

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))

proof end;

theorem :: FUNCT_7:88

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

proof end;

theorem :: FUNCT_7:89

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

proof end;

theorem :: FUNCT_7:90

for f being Function
for n being Element of NAT holds iter (f,n) = compose ((n |-> f),(field f))

proof end;

begin

theorem :: FUNCT_7:91

for f, g being Function
for x, y being set st g c= f & not x in dom g holds
g c= f +* (x,y)

proof end;

theorem :: FUNCT_7:92

for f, g being Function
for A being set st f | A = g | A & f,g equal_outside A holds
f = g

proof end;

theorem :: FUNCT_7:93

for f being Function
for a, b, A being set st a in A holds
f,f +* (a,b) equal_outside A

proof end;

theorem Th94: :: FUNCT_7:94

for f being Function
for a, b, A being set holds
( a in A or (f +* (a,b)) | A = f | A )

proof end;

theorem :: FUNCT_7:95

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

proof end;

theorem Th96: :: FUNCT_7:96

for f being Function
for a, b being set holds (f +* (a .--> b)) . a = b

proof end;

theorem :: FUNCT_7:97

for a, b being set holds <*a*> +* (1,b) = <*b*>

proof end;

theorem :: FUNCT_7:98

for f being Function
for x being set st x in dom f holds
f +* (x .--> (f . x)) = f

proof end;

theorem Th99: :: FUNCT_7:99

for w being FinSequence
for r being set
for i being Nat holds len (w +* (i,r)) = len w

proof end;

theorem :: FUNCT_7:100

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)

proof end;

definition

let F be Function;
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
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₁ being set holds verum;
;

end;

:: 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 ) );

registration

let F be Function;
let x, y be set ;
cluster Swap (F,x,y) -> Relation-like Function-like ;
coherence
( Swap (F,x,y) is Relation-like & Swap (F,x,y) is Function-like )

proof end;

end;

theorem Th101: :: FUNCT_7:101

for F being Function
for x, y being set holds dom (Swap (F,x,y)) = dom F

proof end;

theorem Th102: :: FUNCT_7:102

for F being Function
for x, y being set holds rng (F +* (x,y)) c= (rng F) \/ {y}

proof end;

theorem Th103: :: FUNCT_7:103

for F being Function
for x, y being set holds rng F c= (rng (F +* (x,y))) \/ {(F . x)}

proof end;

theorem Th104: :: FUNCT_7:104

for F being Function
for x, y being set st x in dom F holds
y in rng (F +* (x,y))

proof end;

theorem :: FUNCT_7:105

for F being Function
for x, y being set holds rng (Swap (F,x,y)) = rng F

proof end;

scheme :: FUNCT_7:sch 6
Sch6{ F₁() -> set , F₂() -> non empty set , F₃( set ) -> set } :

F₁(), { F₃(d) where d is Element of F₂() : d in F₁() } are_equipotent

provided

A1: F₁() c= F₂() and
A2: for d1, d2 being Element of F₂() st d1 in F₁() & d2 in F₁() & F₃(d1) = F₃(d2) holds
d1 = d2

proof end;

theorem :: FUNCT_7:106

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

proof end;

theorem :: FUNCT_7:107

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

proof end;

theorem :: FUNCT_7:108

for f, g, h being Function holds
( f +* h = g +* h iff f,g equal_outside dom h )

proof end;

theorem Th109: :: FUNCT_7:109

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

proof end;

theorem :: FUNCT_7:110

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))

proof end;

theorem :: FUNCT_7:111

for f being Function
for x being set st x in dom f holds
f +* (x .--> (f . x)) = f

proof end;

theorem Th112: :: FUNCT_7:112

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

proof end;

theorem :: FUNCT_7:113

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

proof end;

theorem :: FUNCT_7:114

for f being Function
for d, r being set st d in dom f holds
dom f = dom (f +* (d .--> r))

proof end;

theorem :: FUNCT_7:115

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 )

proof end;

theorem :: FUNCT_7:116

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

proof end;

theorem Th117: :: FUNCT_7:117

for A, B, a, b being set
for f being Function of A,B st b in B holds
f +* (a,b) is Function of A,B

proof end;

theorem Th118: :: FUNCT_7:118

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

proof end;

theorem :: FUNCT_7:119

for f, g being Function
for x, y being set holds (f +* g) +~ (x,y) = (f +~ (x,y)) +* (g +~ (x,y))

proof end;

definition

let a, b be set ;
func a followed_by b -> set equals :: FUNCT_7:def 13
(NAT --> b) +* (0,a);
coherence
(NAT --> b) +* (0,a) is set ;

end;

:: deftheorem defines followed_by FUNCT_7:def 13 :
for a, b being set holds a followed_by b = (NAT --> b) +* (0,a);

registration

let a, b be set ;
cluster a followed_by b -> Relation-like Function-like ;
coherence
( a followed_by b is Function-like & a followed_by b is Relation-like ) ;

end;

theorem Th120: :: FUNCT_7:120

for a, b being set holds dom (a followed_by b) = NAT

proof end;

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

proof end;

end;

theorem Th121: :: FUNCT_7:121

for a, b being set holds (a followed_by b) . 0 = a

proof end;

theorem Th122: :: FUNCT_7:122

for a, b being set
for n being Nat st n > 0 holds
(a followed_by b) . n = b

proof end;

definition

let a, b, c be set ;
func (a,b) followed_by c -> set equals :: FUNCT_7:def 14
(NAT --> c) +* ((0,1) --> (a,b));
coherence
(NAT --> c) +* ((0,1) --> (a,b)) is set ;

end;

:: 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));

registration

let a, b, c be set ;
cluster (a,b) followed_by c -> Relation-like Function-like ;
coherence
( (a,b) followed_by c is Function-like & (a,b) followed_by c is Relation-like ) ;

end;

theorem Th123: :: FUNCT_7:123

for a, b, c being set holds dom ((a,b) followed_by c) = NAT

proof end;

theorem Th124: :: FUNCT_7:124

for a, b, c being set holds ((a,b) followed_by c) . 0 = a

proof end;

theorem Th125: :: FUNCT_7:125

for a, b, c being set holds ((a,b) followed_by c) . 1 = b

proof end;

theorem Th126: :: FUNCT_7:126

for a, b, c being set
for n being Nat st n > 1 holds
((a,b) followed_by c) . n = c

proof end;

theorem Th127: :: FUNCT_7:127

for a, b, c being set holds (a,b) followed_by c = (a followed_by c) +* (1,b)

proof end;

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

proof end;

end;

theorem Th128: :: FUNCT_7:128

for a, b being set holds rng (a followed_by b) = {a,b}

proof end;

theorem :: FUNCT_7:129

for a, b, c being set holds rng ((a,b) followed_by c) = {a,b,c}

proof end;

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

proof end;

end;

theorem :: FUNCT_7:130

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

proof end;

theorem :: FUNCT_7:131

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))

proof end;

theorem Th132: :: FUNCT_7:132

for A being set
for f being Function
for g being b₁ -defined Function holds f,f +* g equal_outside A

proof end;

theorem :: FUNCT_7:133

for A being set
for f, g being b₁ -defined Function holds f,g equal_outside A

proof end;

theorem :: FUNCT_7:134

for A being set
for f, g being b₁ -defined Function
for h being Function holds h +* f,h +* g equal_outside A

proof end;

theorem :: FUNCT_7:135

for m being Element of NAT
for I being NAT -defined Function holds card (Shift (I,m)) = card I

proof end;

theorem Th136: :: FUNCT_7:136

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

proof end;

theorem Th137: :: FUNCT_7:137

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

proof end;

theorem :: FUNCT_7:138

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

proof end;

theorem :: FUNCT_7:139

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

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;
cluster f +* (x,y) -> V -valued ;
coherence
f +* (x,y) is V -valued

proof end;

end;

theorem :: FUNCT_7:140

for f, g being Function
for x, y being set st f c= g & not x in dom f holds
f c= g +* (x,y)

proof end;

theorem :: FUNCT_7:141

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)

proof end;