:: Miscellaneous Facts about Functions
:: by Grzegorz Bancerek and Andrzej Trybulec
::
:: Received January 12, 1996
:: Copyright (c) 1996-2012 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
proofend;

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

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

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

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

theorem Th6: :: FUNCT_7:6
for f being Function
for a being set st a in dom f holds
f | {a} = a .--> (f . a)
proofend;

registration
let x, y be set ;
clusterx .--> 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}
proofend;

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

theorem Th9: :: FUNCT_7:9
for f, g, h being Function st rng h c= dom f holds
f * (g +* h) = (f * g) +* (f * h)
proofend;

theorem Th10: :: FUNCT_7:10
for f, g, h being Function holds (g +* h) * f = (g * f) +* (h * f)
proofend;

theorem :: FUNCT_7:11
for f, g, h being Function st rng f misses dom g holds
(h +* g) * f = h * f
proofend;

theorem Th12: :: FUNCT_7:12
for A, B, y being set st A meets rng ((id B) +* (A --> y)) holds
y in A
proofend;

theorem :: FUNCT_7:13
for x, y, A being set st x <> y holds
not x in rng ((id A) +* (x .--> y))
proofend;

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

theorem :: FUNCT_7:15
for f being Function
for X, y, z being set holds (f +* (X --> y)) +* (X --> z) = f +* (X --> z)
proofend;

theorem :: FUNCT_7:16
INT <> INT *
proofend;

theorem :: FUNCT_7:17
{} * = {{}}
proofend;

theorem Th18: :: FUNCT_7:18
for x, A being set holds
( <*x*> in A * iff x in A )
proofend;

theorem :: FUNCT_7:19
for A, B being set st A * c= B * holds
A c= B
proofend;

theorem :: FUNCT_7:20
for A being Subset of NAT st ( for n, m being Element of NAT st n in A &amp; m < n holds
m in A ) holds
A is Cardinal
proofend;

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

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 &amp; i + 1 in dom p ) )
proofend;

registration
cluster non empty Relation-like non-empty NAT -defined Function-like Function-yielding finite FinSequence-like FinSubsequence-like for set ;
existence
 ex b1 being FinSequence st
( b1 is Function-yielding &amp; not b1 is empty &amp; b1 is non-empty )
proofend;
end;

registration
cluster empty Relation-like Function-like  ->  Function-yielding for set ;
coherence
 for b1 being Function st b1 is empty holds
b1 is Function-yielding ;
let f be Function;
cluster<*f*> ->  Function-yielding ;
coherence
 <*f*> is Function-yielding
proofend;
let g be Function;
cluster<*f,g*> ->  Function-yielding ;
coherence
 <*f,g*> is Function-yielding
proofend;
let h be Function;
cluster<*f,g,h*> ->  Function-yielding ;
coherence
 <*f,g,h*> is Function-yielding
proofend;
end;

registration
let n be Element of NAT ;
let f be Function;
clustern |-> f ->  Function-yielding ;
coherence
 n |-> f is Function-yielding ;
end;

registration
let p, q be Function-yielding FinSequence;
clusterp ^ q ->  Function-yielding ;
coherence
 p ^ q is Function-yielding
proofend;
end;

theorem Th23: :: FUNCT_7:23
for p, q being FinSequence st p ^ q is Function-yielding holds
( p is Function-yielding &amp; q is Function-yielding )
proofend;

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

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

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

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

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*>]
proofend;

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:24
for x, A, B being set st x in A /\ B holds
In (x,A) = In (x,B)
proofend;

definition
let f, g be Function;
let A be set ;
predf,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 Th25: :: FUNCT_7:25
for f being Function
for A being set holds f,f equal_outside A
proofend;

theorem Th26: :: FUNCT_7:26
for f, g being Function
for A being set st f,g equal_outside A holds
g,f equal_outside A
proofend;

theorem Th27: :: FUNCT_7:27
for f, g, h being Function
for A being set st f,g equal_outside A &amp; g,h equal_outside A holds
f,h equal_outside A
proofend;

theorem Th28: :: FUNCT_7:28
for f, g being Function
for A being set st f,g equal_outside A holds
(dom f) \ A = (dom g) \ A
proofend;

theorem Th29: :: FUNCT_7:29
for f, g being Function
for A being set st dom g c= A holds
f,f +* g equal_outside A
proofend;

definition
let f be Function;
let i, x be set ;
funcf +* (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 ) &amp; ( 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) ) &amp; ( not i in dom f implies f +* (i,x) = f ) );

theorem Th30: :: FUNCT_7:30
for f being Function
for d, i being set holds dom (f +* (i,d)) = dom f
proofend;

theorem Th31: :: FUNCT_7:31
for f being Function
for d, i being set st i in dom f holds
(f +* (i,d)) . i = d
proofend;

theorem Th32: :: FUNCT_7:32
for f being Function
for d, i, j being set st i <> j holds
(f +* (i,d)) . j = f . j
proofend;

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

theorem :: FUNCT_7:34
for f being Function
for d, e, i being set holds (f +* (i,d)) +* (i,e) = f +* (i,e)
proofend;

theorem Th35: :: FUNCT_7:35
for f being Function
for i being set holds f +* (i,(f . i)) = f
proofend;

registration
let f be FinSequence;
let i, x be set ;
clusterf +* (i,x) ->  FinSequence-like ;
coherence
 f +* (i,x) is FinSequence-like
proofend;
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 funcf +* (i,d) ->  FinSequence of D;
coherence
 f +* (i,d) is FinSequence of D
proofend;
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
proofend;

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 &amp; j in dom f holds
(f +* (i,d)) /. j = f /. j
proofend;

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

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) &amp; f . 0 = id X &amp; ( for i being Element of NAT st i + 1 in dom p holds
for g, h being Function st g = f . i &amp; 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) &amp; f . 0 = id X &amp; ( for i being Element of NAT st i + 1 in dom p holds
for g, h being Function st g = f . i &amp; h = p . (i + 1) holds
f . (i + 1) = h * g ) ) &amp; ex f being ManySortedFunction of NAT st
( b2 = f . (len p) &amp; f . 0 = id X &amp; ( for i being Element of NAT st i + 1 in dom p holds
for g, h being Function st g = f . i &amp; h = p . (i + 1) holds
f . (i + 1) = h * g ) ) holds
b1 = b2
proofend;
correctness
existence
ex b1 being Function ex f being ManySortedFunction of NAT st
( b1 = f . (len p) &amp; f . 0 = id X &amp; ( for i being Element of NAT st i + 1 in dom p holds
for g, h being Function st g = f . i &amp; h = p . (i + 1) holds
f . (i + 1) = h * g ) );
proofend;
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) &amp; f . 0 = id X &amp; ( for i being Element of NAT st i + 1 in dom p holds
for g, h being Function st g = f . i &amp; 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 &amp; it . 1 = x &amp; ( for i being Element of NAT
for f being Function st i in dom p &amp; f = p . i holds
it . (i + 1) = f . (it . i) ) );
existence
 ex b1 being FinSequence st
( len b1 = (len p) + 1 &amp; b1 . 1 = x &amp; ( for i being Element of NAT
for f being Function st i in dom p &amp; f = p . i holds
b1 . (i + 1) = f . (b1 . i) ) )
proofend;
correctness
uniqueness
for b1, b2 being FinSequence st len b1 = (len p) + 1 &amp; b1 . 1 = x &amp; ( for i being Element of NAT
for f being Function st i in dom p &amp; f = p . i holds
b1 . (i + 1) = f . (b1 . i) ) &amp; len b2 = (len p) + 1 &amp; b2 . 1 = x &amp; ( for i being Element of NAT
for f being Function st i in dom p &amp; f = p . i holds
b2 . (i + 1) = f . (b2 . i) ) holds
b1 = b2;
proofend;
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 &amp; b3 . 1 = x &amp; ( for i being Element of NAT
for f being Function st i in dom p &amp; f = p . i holds
b3 . (i + 1) = f . (b3 . i) ) ) );

theorem Th39: :: FUNCT_7:39
for X being set holds compose ({},X) = id X
proofend;

theorem Th40: :: FUNCT_7:40
for x being set holds apply ({},x) = <*x*>
proofend;

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

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

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

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

theorem Th45: :: FUNCT_7:45
for X being set
for f being Function holds compose (<*f*>,X) = f * (id X)
proofend;

theorem :: FUNCT_7:46
for X being set
for f being Function st dom f c= X holds
compose (<*f*>,X) = f
proofend;

theorem Th47: :: FUNCT_7:47
for x being set
for f being Function holds apply (<*f*>,x) = <*x,(f . x)*>
proofend;

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

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

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

theorem Th51: :: FUNCT_7:51
for X being set
for f, g being Function holds compose (<*f,g*>,X) = (g * f) * (id X)
proofend;

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

theorem Th53: :: FUNCT_7:53
for x being set
for f, g being Function holds apply (<*f,g*>,x) = <*x,(f . x),(g . (f . x))*>
proofend;

theorem Th54: :: FUNCT_7:54
for X being set
for f, g, h being Function holds compose (<*f,g,h*>,X) = ((h * g) * f) * (id X)
proofend;

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

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

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 ) &amp; ( F is empty implies ex b1 being set st b1 is empty ) &amp; ( not F is empty implies ex b1 being set st b1 = proj1 (F . 1) ) );
uniqueness
for b1, b2 being set holds
( ( F is empty &amp; b1 is empty &amp; b2 is empty implies b1 = b2 ) &amp; ( not F is empty &amp; b1 = proj1 (F . 1) &amp; 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 ) &amp; ( F is empty implies ex b1 being set st b1 is empty ) &amp; ( 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 &amp; b1 is empty &amp; b2 is empty implies b1 = b2 ) &amp; ( not F is empty &amp; b1 = proj2 (F . (len F)) &amp; 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 ) ) &amp; ( 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 ) ) &amp; ( not F is empty implies ( b2 = lastrng F iff b2 = proj2 (F . (len F)) ) ) );

theorem Th57: :: FUNCT_7:57
( firstdom {} = {} &amp; lastrng {} = {} ) by Def6, Def7;

theorem Th58: :: FUNCT_7:58
for f being Function
for p being FinSequence holds
( firstdom (<*f*> ^ p) = dom f &amp; lastrng (p ^ <*f*>) = rng f )
proofend;

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

definition
let IT be FinSequence;
attrIT is FuncSeq-like  means :Def8: :: FUNCT_7:def 8
 ex p being FinSequence st
( len p = (len IT) + 1 &amp; ( 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 &amp; ( for i being Element of NAT st i in dom IT holds
IT . i in Funcs ((p . i),(p . (i + 1))) ) ) );

theorem Th60: :: FUNCT_7:60
for p, q being FinSequence st p ^ q is FuncSeq-like holds
( p is FuncSeq-like &amp; q is FuncSeq-like )
proofend;

registration
cluster Relation-like Function-like FinSequence-like FuncSeq-like  ->  Function-yielding for set ;
coherence
 for b1 being FinSequence st b1 is FuncSeq-like holds
b1 is Function-yielding
proofend;
end;

registration
cluster empty Relation-like Function-like FinSequence-like  ->  FuncSeq-like for set ;
coherence
 for b1 being FinSequence st b1 is empty holds
b1 is FuncSeq-like
proofend;
end;

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

registration
cluster non empty Relation-like non-empty NAT -defined Function-like finite FinSequence-like FinSubsequence-like FuncSeq-like for set ;
existence
 ex b1 being FinSequence st
( b1 is FuncSeq-like &amp; not b1 is empty &amp; b1 is non-empty )
proofend;
end;

definition
mode FuncSequence is FuncSeq-like FinSequence;
end;

theorem Th61: :: FUNCT_7:61
for X being set
for p being FuncSequence st p <> {} holds
dom (compose (p,X)) = (firstdom p) /\ X
proofend;

theorem Th62: :: FUNCT_7:62
for p being FuncSequence holds dom (compose (p,(firstdom p))) = firstdom p
proofend;

theorem :: FUNCT_7:63
for p being FuncSequence
for f being Function st rng f c= firstdom p holds
<*f*> ^ p is FuncSequence
proofend;

theorem :: FUNCT_7:64
for p being FuncSequence
for f being Function st lastrng p c= dom f holds
p ^ <*f*> is FuncSequence
proofend;

theorem :: FUNCT_7:65
for x, X being set
for p being FuncSequence st x in firstdom p &amp; x in X holds
(apply (p,x)) . ((len p) + 1) = (compose (p,X)) . x
proofend;

definition
let X, Y be set ;
assume X1: ( Y is empty implies X is empty ) ;
mode FuncSequence of X,Y ->  FuncSequence means :Def9: :: FUNCT_7:def 9
( firstdom it = X &amp; lastrng it c= Y );
existence
 ex b1 being FuncSequence st
( firstdom b1 = X &amp; lastrng b1 c= Y )
proofend;
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 &amp; 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
proofend;
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 &amp; ( 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 &amp; ( for i being Element of NAT st i in dom b1 holds
b1 . i in Funcs ((q . i),(q . (i + 1))) ) )
proofend;
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 &amp; ( 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 for FuncSequence of q;
coherence
 for b1 being FuncSequence of q holds
( b1 is FuncSeq-like &amp; b1 is non-empty )
proofend;
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 &amp; lastrng p c= q . (len q) )
proofend;

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 &amp; rng (compose (p,(q . 1))) c= q . (len q) )
proofend;

:: Moved from FUNCT_4
registration
let X be set ;
let f be Function of NAT,(bool [:X,X:]);
let n be Nat;
clusterf . n ->  Relation-like ;
coherence
 f . n is Relation-like
proofend;
end;

Lm1:  for X being set
for f being Function of X,X holds rng f c= dom f
proofend;

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) &amp; ( for k being Nat holds p1 . (k + 1) = f * (p1 . k) ) &amp; p2 . 0 = id (field f) &amp; ( for k being Nat holds p2 . (k + 1) = f * (p2 . k) ) holds
p1 = p2
proofend;

definition
let f be Relation;
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 &amp; p . 0 = id (field f) &amp; ( for k being Nat holds p . (k + 1) = f * (p . k) ) );
existence
 ex b1 being Relation ex p being Function of NAT,(bool [:(field f),(field f):]) st
( b1 = p . n &amp; p . 0 = id (field f) &amp; ( for k being Nat holds p . (k + 1) = f * (p . k) ) )
proofend;
uniqueness
 for b1, b2 being Relation st ex p being Function of NAT,(bool [:(field f),(field f):]) st
( b1 = p . n &amp; p . 0 = id (field f) &amp; ( for k being Nat holds p . (k + 1) = f * (p . k) ) ) &amp; ex p being Function of NAT,(bool [:(field f),(field f):]) st
( b2 = p . n &amp; p . 0 = id (field f) &amp; ( for k being Nat holds p . (k + 1) = f * (p . k) ) ) holds
b1 = b2 by Lm2;
end;

:: deftheorem Def11 defines iter FUNCT_7:def_11_:_
 for f being Relation
for n being Nat
for b3 being Relation holds
( b3 = iter (f,n) iff ex p being Function of NAT,(bool [:(field f),(field f):]) st
( b3 = p . n &amp; p . 0 = id (field f) &amp; ( for k being Nat holds p . (k + 1) = f * (p . k) ) ) );

registration
let f be Function;
let n be Nat;
cluster iter (f,n) ->  Function-like ;
coherence
 iter (f,n) is Function-like
proofend;
end;

Lm3:  for R being Relation holds
( (id (field R)) * R = R &amp; R * (id (field R)) = R )
proofend;

theorem Th68: :: FUNCT_7:68
for R being Relation holds iter (R,0) = id (field R)
proofend;

Lm4:  for R being Relation st rng R c= dom R holds
iter (R,0) = id (dom R)
proofend;

theorem Th69: :: FUNCT_7:69
for R being Relation
for n being Nat holds iter (R,(n + 1)) = R * (iter (R,n))
proofend;

theorem Th70: :: FUNCT_7:70
for R being Relation holds iter (R,1) = R
proofend;

theorem Th71: :: FUNCT_7:71
for R being Relation
for n being Nat holds iter (R,(n + 1)) = (iter (R,n)) * R
proofend;

theorem Th72: :: FUNCT_7:72
for n being Element of NAT
for R being Relation holds
( dom (iter (R,n)) c= field R &amp; rng (iter (R,n)) c= field R )
proofend;

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 &amp; rng (iter (R,n)) c= rng R )
proofend;

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 &amp; rng (iter (R,n)) c= dom R )
proofend;

theorem Th75: :: FUNCT_7:75
for n being Element of NAT
for R being Relation holds (id (field R)) * (iter (R,n)) = iter (R,n)
proofend;

theorem :: FUNCT_7:76
for n being Element of NAT
for R being Relation holds (iter (R,n)) * (id (field R)) = iter (R,n)
proofend;

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

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

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

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

theorem :: FUNCT_7:80
for n being Element of NAT holds iter ({},n) = {}
proofend;

theorem :: FUNCT_7:81
for X being set
for n being Element of NAT holds iter ((id X),n) = id X
proofend;

theorem :: FUNCT_7:82
for R being Relation st rng R misses dom R holds
iter (R,2) = {}
proofend;

theorem :: FUNCT_7:83
for X being set
for n being Nat
for f being Function of X,X holds iter (f,n) is Function of X,X
proofend;

theorem :: FUNCT_7:84
for X being set
for f being Function of X,X holds iter (f,0) = id X
proofend;

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

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

theorem :: FUNCT_7:87
for a, X being set
for f being Function
for n being Element of NAT st n <> 0 &amp; a in X &amp; f = X --> a holds
iter (f,n) = f
proofend;

theorem :: FUNCT_7:88
for f being Function
for n being Element of NAT holds iter (f,n) = compose ((n |-> f),(field f))
proofend;

begin

:: from SCMFSA6A, 2006.03.14, A.T.
theorem :: FUNCT_7:89
for f, g being Function
for x, y being set st g c= f &amp; not x in dom g holds
g c= f +* (x,y)
proofend;

theorem :: FUNCT_7:90
for f, g being Function
for A being set st f | A = g | A &amp; f,g equal_outside A holds
f = g
proofend;

theorem :: FUNCT_7:91
for f being Function
for a, b, A being set st a in A holds
f,f +* (a,b) equal_outside A
proofend;

theorem Th92: :: FUNCT_7:92
for f being Function
for a, b, A being set holds
( a in A or (f +* (a,b)) | A = f | A )
proofend;

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

:: from YELLOW14, 2006.03.14, A.T.
theorem Th94: :: FUNCT_7:94
for f being Function
for a, b being set holds (f +* (a .--> b)) . a = b
proofend;

:: from SCMFSA6A, 2006.03.14, A.T.
theorem :: FUNCT_7:95
for a, b being set holds <*a*> +* (1,b) = <*b*>
proofend;

:: from SCMFSA8C, 2006.03.15
theorem :: FUNCT_7:96
for f being Function
for x being set st x in dom f holds
f +* (x .--> (f . x)) = f
proofend;

theorem Th97: :: FUNCT_7:97
for w being FinSequence
for r being set
for i being Nat holds len (w +* (i,r)) = len w
proofend;

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

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 &amp; y in dom F )
otherwise F;
correctness
coherence
( ( x in dom F &amp; y in dom F implies (F +* (x,(F . y))) +* (y,(F . x)) is set ) &amp; ( ( 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 &amp; y in dom F implies Swap (F,x,y) = (F +* (x,(F . y))) +* (y,(F . x)) ) &amp; ( ( 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 &amp; Swap (F,x,y) is Function-like )
proofend;
end;

theorem Th99: :: FUNCT_7:99
for F being Function
for x, y being set holds dom (Swap (F,x,y)) = dom F
proofend;

theorem Th100: :: FUNCT_7:100
for F being Function
for x, y being set holds rng (F +* (x,y)) c= (rng F) \/ {y}
proofend;

theorem Th101: :: FUNCT_7:101
for F being Function
for x, y being set holds rng F c= (rng (F +* (x,y))) \/ {(F . x)}
proofend;

theorem Th102: :: FUNCT_7:102
for F being Function
for x, y being set st x in dom F holds
y in rng (F +* (x,y))
proofend;

theorem :: FUNCT_7:103
for F being Function
for x, y being set holds rng (Swap (F,x,y)) = rng F
proofend;

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() &amp; d2 in F1() &amp; F3(d1) = F3(d2) holds
d1 = d2
proofend;

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

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

theorem :: FUNCT_7:106
for f, g, h being Function holds
( f +* h = g +* h iff f,g equal_outside dom h )
proofend;

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

theorem :: FUNCT_7:108
for x, y being set
for f being Function st ( x in dom f implies ( y in dom f &amp; f . x = f . y ) ) holds
f = f * ((id (dom f)) +* (x,y))
proofend;

:: from SCMFSA8C, 2007.07.26, A.T.
theorem :: FUNCT_7:109
for f being Function
for x being set st x in dom f holds
f +* (x .--> (f . x)) = f
proofend;

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

theorem :: FUNCT_7:111
for f being Function
for x, y being set st x in dom f &amp; y in dom f holds
ex p being Permutation of (dom f) st (f +* (x,(f . y))) +* (y,(f . x)) = f * p
proofend;

:: from SCMISORT, 2007.07.26, A.T.
theorem :: FUNCT_7:112
for f being Function
for d, r being set st d in dom f holds
dom f = dom (f +* (d .--> r))
proofend;

:: 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 &amp; n <= len f &amp; 1 <= m &amp; m <= len f &amp; g = (f +* (m,(f /. n))) +* (n,(f /. m)) holds
( f . m = g . n &amp; f . n = g . m &amp; ( for k being set st k <> m &amp; k <> n &amp; k in dom f holds
f . k = g . k ) &amp; f,g are_fiberwise_equipotent )
proofend;

:: 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 &amp; a <> c holds
(((f +* (a .--> A)) +* (b .--> B)) +* (c .--> C)) . a = A
proofend;

:: comp TOPALG_3:1, 2008.01.18, A.T.
theorem Th115: :: FUNCT_7:115
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
proofend;

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

theorem :: FUNCT_7:117
for f, g being Function
for x, y being set holds (f +* g) +~ (x,y) = (f +~ (x,y)) +* (g +~ (x,y))
proofend;

definition
let a, b be set ;
funca 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 ;
clustera followed_by b ->  Relation-like Function-like ;
coherence
 ( a followed_by b is Function-like &amp; a followed_by b is Relation-like ) ;
end;

theorem Th118: :: FUNCT_7:118
for a, b being set holds dom (a followed_by b) = NAT
proofend;

definition
let X be non empty set ;
let a, b be Element of X;
:: original:followed_by
redefine funca followed_by b ->  sequence of X;
coherence
 a followed_by b is sequence of X
proofend;
end;

theorem Th119: :: FUNCT_7:119
for a, b being set holds (a followed_by b) . 0 = a
proofend;

theorem Th120: :: FUNCT_7:120
for a, b being set
for n being Nat st n > 0 holds
(a followed_by b) . n = b
proofend;

:: from DYNKIN, 2008.09.24, A.T.
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 &amp; (a,b) followed_by c is Relation-like ) ;
end;

theorem Th121: :: FUNCT_7:121
for a, b, c being set holds dom ((a,b) followed_by c) = NAT
proofend;

theorem Th122: :: FUNCT_7:122
for a, b, c being set holds ((a,b) followed_by c) . 0 = a
proofend;

theorem Th123: :: FUNCT_7:123
for a, b, c being set holds ((a,b) followed_by c) . 1 = b
proofend;

theorem Th124: :: FUNCT_7:124
for a, b, c being set
for n being Nat st n > 1 holds
((a,b) followed_by c) . n = c
proofend;

theorem Th125: :: FUNCT_7:125
for a, b, c being set holds (a,b) followed_by c = (a followed_by c) +* (1,b)
proofend;

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
proofend;
end;

theorem Th126: :: FUNCT_7:126
for a, b being set holds rng (a followed_by b) = {a,b}
proofend;

theorem :: FUNCT_7:127
for a, b, c being set holds rng ((a,b) followed_by c) = {a,b,c}
proofend;

:: 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 funcf +* (x,y) ->  Function of A,B;
coherence
 f +* (x,y) is Function of A,B
proofend;
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
proofend;

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

theorem Th130: :: FUNCT_7:130
for A being set
for f being Function
for g being b1 -defined Function holds f,f +* g equal_outside A
proofend;

theorem :: FUNCT_7:131
for A being set
for f, g being b1 -defined Function holds f,g equal_outside A
proofend;

theorem :: FUNCT_7:132
for A being set
for f, g being b1 -defined Function
for h being Function holds h +* f,h +* g equal_outside A
proofend;

theorem :: FUNCT_7:133
for m being Element of NAT
for I being NAT -defined Function holds card (Shift (I,m)) = card I
proofend;

theorem Th134: :: FUNCT_7:134
for A, B being set
for f, g being Function st dom f = dom g &amp; dom f c= A \/ B &amp; f | B = g | B holds
f,g equal_outside A
proofend;

theorem Th135: :: FUNCT_7:135
for B, A being set
for f, g being Function st dom f = dom g &amp; B c= dom f &amp; A misses B &amp; f,g equal_outside A holds
f | B = g | B
proofend;

theorem :: FUNCT_7:136
for I, A, B being set
for X, Y being ManySortedSet of I st I c= A \/ B &amp; X | B = Y | B holds
X,Y equal_outside A
proofend;

theorem :: FUNCT_7:137
for B, I, A being set
for X, Y being ManySortedSet of I st B c= I &amp; A misses B &amp; X,Y equal_outside A holds
X | B = Y | B
proofend;

registration
let V be non empty set ;
let f be V -valued Function;
let x be set ;
let y be Element of V;
clusterf +* (x,y) -> V -valued ;
coherence
 f +* (x,y) is V -valued
proofend;
end;

theorem :: FUNCT_7:138
for f, g being Function
for x, y being set st f c= g &amp; not x in dom f holds
f c= g +* (x,y)
proofend;

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