:: 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 b1 being FinSequence st
( b1 is Function-yielding & not b1 is empty & b1 is non-empty )
proof end;
end;

registration
cluster empty Relation-like Function-like -> Function-yielding set ;
coherence
for b1 being Function st b1 is empty holds
b1 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{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , F4( Element of F1(), Element of F2()) -> set } :
ex f being Function of [:F1(),F2():],F3() st
for x being Element of F1()
for y being Element of F2() holds f . (x,y) = F4(x,y)
provided
A1: for x being Element of F1()
for y being Element of F2() holds F4(x,y) in F3()
proof end;

scheme :: FUNCT_7:sch 2
FinMono{ F1() -> set , F2() -> non empty set , F3( set ) -> set , F4( set ) -> set } :
{ F3(d) where d is Element of F2() : F4(d) in F1() } is finite
provided
A1: F1() is finite and
A2: for d1, d2 being Element of F2() st F4(d1) = F4(d2) holds
d1 = d2
proof end;

scheme :: FUNCT_7:sch 3
CardMono{ F1() -> set , F2() -> non empty set , F3( set ) -> set } :
F1(), { d where d is Element of F2() : F3(d) in F1() } are_equipotent
provided
A1: for x being set st x in F1() holds
ex d being Element of F2() st x = F3(d) and
A2: for d1, d2 being Element of F2() st F3(d1) = F3(d2) holds
d1 = d2
proof end;

scheme :: FUNCT_7:sch 4
CardMono9{ F1() -> set , F2() -> non empty set , F3( set ) -> set } :
F1(), { F3(d) where d is Element of F2() : d in F1() } are_equipotent
provided
A1: F1() c= F2() and
A2: for d1, d2 being Element of F2() st F3(d1) = F3(d2) holds
d1 = d2
proof end;

scheme :: FUNCT_7:sch 5
FuncSeqInd{ P1[ set ] } :
for p being Function-yielding FinSequence holds P1[p]
provided
A1: P1[ {} ] and
A2: for p being Function-yielding FinSequence st P1[p] holds
for f being Function holds P1[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 b1 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 b1, b2 being Function st ex f being ManySortedFunction of NAT st
( b1 = 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
( b2 = 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
b1 = b2
proof end;
correctness
existence
ex b1 being Function ex f being ManySortedFunction of NAT st
( b1 = 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 b3 being Function holds
( b3 = compose (p,X) iff ex f being ManySortedFunction of NAT st
( b3 = 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 b1 being FinSequence st
( len b1 = (len p) + 1 & b1 . 1 = x & ( for i being Element of NAT
for f being Function st i in dom p & f = p . i holds
b1 . (i + 1) = f . (b1 . i) ) )
proof end;
correctness
uniqueness
for b1, b2 being FinSequence st len b1 = (len p) + 1 & b1 . 1 = x & ( for i being Element of NAT
for f being Function st i in dom p & f = p . i holds
b1 . (i + 1) = f . (b1 . i) ) & len b2 = (len p) + 1 & b2 . 1 = x & ( for i being Element of NAT
for f being Function st i in dom p & f = p . i holds
b2 . (i + 1) = f . (b2 . i) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def5 defines apply FUNCT_7:def 5 :
for p being Function-yielding FinSequence
for x being set
for b3 being FinSequence holds
( b3 = apply (p,x) iff ( len b3 = (len p) + 1 & b3 . 1 = x & ( for i being Element of NAT
for f being Function st i in dom p & f = p . i holds
b3 . (i + 1) = f . (b3 . 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 b1 being set holds verum
;
existence
( ( for b1 being set holds verum ) & ( F is empty implies ex b1 being set st b1 is empty ) & ( not F is empty implies ex b1 being set st b1 = proj1 (F . 1) ) )
;
uniqueness
for b1, b2 being set holds
( ( F is empty & b1 is empty & b2 is empty implies b1 = b2 ) & ( not F is empty & b1 = proj1 (F . 1) & b2 = proj1 (F . 1) implies b1 = b2 ) )
;
;
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 b1 being set holds verum
;
existence
( ( for b1 being set holds verum ) & ( F is empty implies ex b1 being set st b1 is empty ) & ( not F is empty implies ex b1 being set st b1 = proj2 (F . (len F)) ) )
;
uniqueness
for b1, b2 being set holds
( ( F is empty & b1 is empty & b2 is empty implies b1 = b2 ) & ( not F is empty & b1 = proj2 (F . (len F)) & b2 = proj2 (F . (len F)) implies b1 = b2 ) )
;
;
end;

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

:: deftheorem Def7 defines lastrng FUNCT_7:def 7 :
for F being FinSequence
for b2 being set holds
( ( F is empty implies ( b2 = lastrng F iff b2 is empty ) ) & ( not F is empty implies ( b2 = lastrng F iff b2 = 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 b1 being FinSequence st b1 is FuncSeq-like holds
b1 is Function-yielding
proof end;
end;

registration
cluster empty Relation-like Function-like FinSequence-like -> FuncSeq-like set ;
coherence
for b1 being FinSequence st b1 is empty holds
b1 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 b1 being FinSequence st
( b1 is FuncSeq-like & not b1 is empty & b1 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 b1 being FuncSequence st
( firstdom b1 = X & lastrng b1 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 b3 being FuncSequence holds
( b3 is FuncSequence of X,Y iff ( firstdom b3 = X & lastrng b3 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 b1 being FinSequence st
( (len b1) + 1 = len q & ( for i being Element of NAT st i in dom b1 holds
b1 . 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 b2 being FinSequence holds
( b2 is FuncSequence of q iff ( (len b2) + 1 = len q & ( for i being Element of NAT st i in dom b2 holds
b2 . 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 b1 being FuncSequence of q holds
( b1 is FuncSeq-like & b1 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 b1 being Function ex p being Function of NAT,(PFuncs ((field f),(field f))) st
( b1 = p . n & p . 0 = id (field f) & ( for k being Nat holds p . (k + 1) = (p . k) * f ) )
proof end;
uniqueness
for b1, b2 being Function st ex p being Function of NAT,(PFuncs ((field f),(field f))) st
( b1 = 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
( b2 = p . n & p . 0 = id (field f) & ( for k being Nat holds p . (k + 1) = (p . k) * f ) ) holds
b1 = b2
by Lm2;
end;

:: deftheorem Def11 defines iter FUNCT_7:def 11 :
for f being Function
for n being Nat
for b3 being Function holds
( b3 = iter (f,n) iff ex p being Function of NAT,(PFuncs ((field f),(field f))) st
( b3 = 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 b1 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{ F1() -> set , F2() -> non empty set , F3( set ) -> set } :
F1(), { F3(d) where d is Element of F2() : d in F1() } are_equipotent
provided
A1: F1() c= F2() and
A2: for d1, d2 being Element of F2() st d1 in F1() & d2 in F1() & F3(d1) = F3(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 b1 -defined Function holds f,f +* g equal_outside A
proof end;

theorem :: FUNCT_7:133
for A being set
for f, g being b1 -defined Function holds f,g equal_outside A
proof end;

theorem :: FUNCT_7:134
for A being set
for f, g being b1 -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;