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

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

cluster x .--> y -> non empty ;

coherence
not x .--> y is empty ;

end;

registration

let x, y, a, b be object ;

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 Th9: :: FUNCT_7:9

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

proof end;

theorem Th10: :: FUNCT_7:10

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

proof end;

theorem :: FUNCT_7:11

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

proof end;

theorem Th12: :: FUNCT_7:12

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

proof end;

theorem :: FUNCT_7:13

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

proof end;

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

proof end;

theorem :: FUNCT_7:15

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

proof end;

theorem :: FUNCT_7:16

INT <> INT *

proof end;

theorem :: FUNCT_7:17

{} * = {{}}

proof end;

theorem Th18: :: FUNCT_7:18

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

proof end;

theorem :: FUNCT_7:19

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

proof end;

theorem :: FUNCT_7:20

for A being Subset of NAT st ( for n, m being Nat st n in A & m < n holds
m in A ) holds
A is Cardinal

proof end;

theorem :: FUNCT_7:21

for A being finite set
for X being non empty Subset-Family of A ex C being Element of X st
for B being Element of X st B c= C holds
B = C

proof end;

theorem Th22: :: FUNCT_7:22

for p, q being FinSequence st len p = (len q) + 1 holds
for i being 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 omega -defined Function-like Function-yielding finite FinSequence-like FinSubsequence-like for 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 for set ;

coherence
for b₁ being Function st b₁ is empty holds
b₁ is Function-yielding ;

end;

registration

let n be 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 Th23: :: FUNCT_7:23

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

proof end;

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₂()) -> object } :

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₃( object ) -> object , F₄( object ) -> object } :

{ 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₃( object ) -> object } :

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₃( object ) -> object } :

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₁[ object ] } :

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;

definition

let f, g be Function;
let A be set ;

pred f,g equal_outside A means :: FUNCT_7:def 2
f | ((dom f) \ A) = g | ((dom g) \ A);

end;

:: deftheorem FUNCT_7:def 1 :
canceled;

:: deftheorem 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 :: FUNCT_7:24

canceled;

::$CT

theorem :: FUNCT_7:25

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

theorem Th25: :: FUNCT_7:26

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

theorem :: FUNCT_7:27

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

theorem Th27: :: 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

proof end;

theorem Th28: :: FUNCT_7:29

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

func f +* (i,x) -> Function equals :Def2: :: 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 Def2 defines +* FUNCT_7:def 3 :
for f being Function
for i, x being object holds
( ( i in dom f implies f +* (i,x) = f +* (i .--> x) ) & ( not i in dom f implies f +* (i,x) = f ) );

theorem Th29: :: FUNCT_7:30

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

proof end;

registration

let f be empty Function;
let i, x be object ;

cluster f +* (i,x) -> empty ;

coherence
f +* (i,x) is empty

proof end;

end;

registration

let f be non empty Function;
let i, x be object ;

cluster f +* (i,x) -> non empty ;

coherence
not f +* (i,x) is empty

proof end;

end;

theorem Th30: :: FUNCT_7:31

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

proof end;

theorem Th31: :: FUNCT_7:32

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

proof end;

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)

proof end;

theorem :: FUNCT_7:34

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

proof end;

theorem Th34: :: FUNCT_7:35

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

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 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:36

for D being non empty set
for f being FinSequence of D
for d being Element of D
for i being Nat st i in dom f holds
(f +* (i,d)) /. i = d

proof end;

theorem :: FUNCT_7:37

for D being non empty set
for f being FinSequence of D
for d being Element of D
for i, j being Nat st i <> j & j in dom f holds
(f +* (i,d)) /. j = f /. j

proof end;

theorem :: FUNCT_7:38

for D being non empty set
for f being FinSequence of D
for d, e being Element of D
for i being Nat holds f +* (i,(f /. i)) = f

proof end;

definition

let X be set ;
let p be Function-yielding FinSequence;

func compose (p,X) -> Function means :Def3: :: FUNCT_7:def 4
ex f being ManySortedFunction of NAT st
( it = f . (len p) & f . 0 = id X & ( for i being 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 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 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 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 Def3 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 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 object ;

func apply (p,x) -> FinSequence means :Def4: :: FUNCT_7:def 5
( len it = (len p) + 1 & it . 1 = x & ( for i being 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 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 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 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 Def4 defines apply FUNCT_7:def 5 :
for p being Function-yielding FinSequence
for x being object
for b₃ being FinSequence holds
( b₃ = apply (p,x) iff ( len b₃ = (len p) + 1 & b₃ . 1 = x & ( for i being Nat
for f being Function st i in dom p & f = p . i holds
b₃ . (i + 1) = f . (b₃ . i) ) ) );

theorem Th38: :: FUNCT_7:39

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

proof end;

theorem Th39: :: FUNCT_7:40

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

proof end;

theorem Th40: :: 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))

proof end;

theorem Th41: :: FUNCT_7:42

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

proof end;

theorem :: FUNCT_7:43

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

proof end;

theorem :: FUNCT_7:44

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

proof end;

theorem Th44: :: FUNCT_7:45

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

proof end;

theorem :: FUNCT_7:46

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

proof end;

theorem Th46: :: FUNCT_7:47

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

proof end;

theorem :: FUNCT_7:48

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

proof end;

theorem Th48: :: FUNCT_7:49

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

proof end;

theorem :: FUNCT_7:50

for x being object
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 Th50: :: FUNCT_7:51

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

proof end;

theorem :: FUNCT_7:52

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

proof end;

theorem Th52: :: FUNCT_7:53

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

proof end;

theorem Th53: :: FUNCT_7:54

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

proof end;

theorem :: FUNCT_7:56

for x being object
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 :Def5: :: 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 :Def6: :: 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 Def5 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 Def6 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 Th56: :: FUNCT_7:57

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

theorem Th57: :: FUNCT_7:58

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

proof end;

theorem Th58: :: FUNCT_7:59

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 :Def7: :: FUNCT_7:def 8
ex p being FinSequence st
( len p = (len IT) + 1 & ( for i being Nat st i in dom IT holds
IT . i in Funcs ((p . i),(p . (i + 1))) ) );

end;

:: deftheorem Def7 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 Nat st i in dom IT holds
IT . i in Funcs ((p . i),(p . (i + 1))) ) ) );

theorem Th59: :: FUNCT_7:60

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 for 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 for 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 omega -defined Function-like finite FinSequence-like FinSubsequence-like FuncSeq-like for 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 Th60: :: FUNCT_7:61

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

proof end;

theorem Th61: :: FUNCT_7:62

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

proof end;

theorem :: FUNCT_7:63

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

proof end;

theorem :: FUNCT_7:64

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

proof end;

theorem :: FUNCT_7:65

for X being set
for x being object
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 :Def8: :: 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 Def8 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 :Def9: :: FUNCT_7:def 10
( (len it) + 1 = len q & ( for i being 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 Nat st i in dom b₁ holds
b₁ . i in Funcs ((q . i),(q . (i + 1))) ) )

proof end;

end;

:: deftheorem Def9 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 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 for FuncSequence of q;

coherence
for b₁ being FuncSequence of q holds
( b₁ is FuncSeq-like & b₁ is non-empty )

proof end;

end;

theorem Th65: :: FUNCT_7:66

for q being non empty non-empty FinSequence
for p being FuncSequence of q st p <> {} holds
( firstdom p = q . 1 & lastrng p c= q . (len q) )

proof end;

theorem :: FUNCT_7:67

for q being non empty non-empty FinSequence
for p being FuncSequence of q holds
( dom (compose (p,(q . 1))) = q . 1 & rng (compose (p,(q . 1))) c= q . (len q) )

proof end;

:: Moved from FUNCT_4

registration

let X be set ;
let f be sequence of (bool [:X,X:]);
let n be Nat;

cluster f . n -> Relation-like ;

coherence
f . n is Relation-like

proof end;

end;

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

proof end;

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

proof end;

definition

let f be Relation;
let n be Nat;

func iter (f,n) -> Relation means :Def10: :: FUNCT_7:def 11
ex p being sequence of (bool [:(field f),(field f):]) st
( it = p . n & p . 0 = id (field f) & ( for k being Nat holds p . (k + 1) = f * (p . k) ) );

existence
ex b₁ being Relation ex p being sequence of (bool [:(field f),(field f):]) st
( b₁ = p . n & p . 0 = id (field f) & ( for k being Nat holds p . (k + 1) = f * (p . k) ) )

proof end;

uniqueness
for b₁, b₂ being Relation st ex p being sequence of (bool [:(field f),(field f):]) st
( b₁ = p . n & p . 0 = id (field f) & ( for k being Nat holds p . (k + 1) = f * (p . k) ) ) & ex p being sequence of (bool [:(field f),(field f):]) st
( b₂ = p . n & p . 0 = id (field f) & ( for k being Nat holds p . (k + 1) = f * (p . k) ) ) holds
b₁ = b₂ by Lm2;

end;

:: deftheorem Def10 defines iter FUNCT_7:def 11 :
for f being Relation
for n being Nat
for b₃ being Relation holds
( b₃ = iter (f,n) iff ex p being sequence of (bool [:(field f),(field f):]) st
( b₃ = p . n & p . 0 = id (field f) & ( 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

proof end;

end;

Lm3: for R being Relation holds
( (id (field R)) * R = R & R * (id (field R)) = R )
by RELAT_1:51, RELAT_1:53, XBOOLE_1:7;

theorem Th67: :: FUNCT_7:68

for R being Relation holds iter (R,0) = id (field R)

proof end;

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

proof end;

theorem Th68: :: FUNCT_7:69

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

proof end;

theorem Th69: :: FUNCT_7:70

for R being Relation holds iter (R,1) = R

proof end;

theorem Th70: :: FUNCT_7:71

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

proof end;

theorem Th71: :: FUNCT_7:72

for n being Nat
for R being Relation holds
( dom (iter (R,n)) c= field R & rng (iter (R,n)) c= field R )

proof end;

theorem :: FUNCT_7:73

for n being Nat
for R being Relation st n <> 0 holds
( dom (iter (R,n)) c= dom R & rng (iter (R,n)) c= rng R )

proof end;

theorem Th73: :: FUNCT_7:74

for R being Relation
for n being Nat st rng R c= dom R holds
( dom (iter (R,n)) = dom R & rng (iter (R,n)) c= dom R )

proof end;

theorem Th74: :: FUNCT_7:75

for n being Nat
for R being Relation holds (id (field R)) * (iter (R,n)) = iter (R,n)

proof end;

theorem :: FUNCT_7:76

for n being Nat
for R being Relation holds (iter (R,n)) * (id (field R)) = iter (R,n)

proof end;

theorem Th76: :: FUNCT_7:77

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

proof end;

Lm5: for m, k being Nat
for R being Relation st iter ((iter (R,m)),k) = iter (R,(m * k)) holds
iter ((iter (R,m)),(k + 1)) = iter (R,(m * (k + 1)))

proof end;

theorem :: FUNCT_7:78

for m, n being Nat
for R being Relation st n <> 0 holds
iter ((iter (R,m)),n) = iter (R,(m * n))

proof end;

theorem Th78: :: FUNCT_7:79

for m, n being Nat
for R being Relation st rng R c= dom R holds
iter ((iter (R,m)),n) = iter (R,(m * n))

proof end;

theorem :: FUNCT_7:80

for n being Nat holds iter ({},n) = {}

proof end;

theorem :: FUNCT_7:81

for X being set
for n being Nat holds iter ((id X),n) = id X

proof end;

theorem :: FUNCT_7:82

for R being Relation st rng R misses dom R holds
iter (R,2) = {}

proof end;

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

proof end;

theorem :: FUNCT_7:84

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

proof end;

theorem :: FUNCT_7:85

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

proof end;

theorem :: FUNCT_7:86

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

proof end;

theorem :: FUNCT_7:87

for a being object
for X being set
for f being Function
for n being Nat st n <> 0 & a in X & f = X --> a holds
iter (f,n) = f

proof end;

theorem :: FUNCT_7:88

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

proof end;

:: 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 & not x in dom g holds
g c= f +* (x,y)

proof end;

theorem :: FUNCT_7:90

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:91

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 Th91: :: FUNCT_7:92

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

proof end;

theorem :: FUNCT_7:93

for f, g being Function
for a, b being object
for A being set st f | A = g | A holds
(f +* (a,b)) | A = (g +* (a,b)) | A

proof end;

:: from YELLOW14, 2006.03.14, A.T.

theorem Th93: :: FUNCT_7:94

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

proof end;

:: from SCMFSA6A, 2006.03.14, A.T.

theorem :: FUNCT_7:95

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

proof end;

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

proof end;

theorem Th96: :: FUNCT_7:97

for w being FinSequence
for r being object
for i being natural Number holds len (w +* (i,r)) = len w

proof end;

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)

proof end;

definition

let F be Function;
let x, y be object ;

func Swap (F,x,y) -> set equals :Def11: :: 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 Def11 defines Swap FUNCT_7:def 12 :
for F being Function
for x, y being object 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 object ;

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 Th98: :: FUNCT_7:99

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

proof end;

theorem Th99: :: FUNCT_7:100

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

proof end;

theorem Th100: :: FUNCT_7:101

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

proof end;

theorem Th101: :: FUNCT_7:102

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

proof end;

theorem :: FUNCT_7:103

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

proof end;

:: from SCMFSA_7, 2007.07.22, A.T.

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

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;

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

proof end;

theorem :: FUNCT_7:105

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

proof end;

theorem :: FUNCT_7:106

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

proof end;

:: from SF_MASTR, 2007.07.25, A.T.

theorem Th106: :: FUNCT_7:107

for x, y, a being object
for f being Function st f . x = f . y holds
f . a = (f * ((id (dom f)) +* (x,y))) . a

proof end;

theorem :: FUNCT_7:108

for x, y being set
for f being Function st ( x in dom f implies ( y in dom f & f . x = f . y ) ) holds
f = f * ((id (dom f)) +* (x,y))

proof end;

theorem :: FUNCT_7:109

canceled;

::$CT
:: from SFMASTR3, 2007.07.26, A.T.

theorem Th109: :: 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

proof end;

theorem :: FUNCT_7:111

for f being Function
for x, y being set st x in dom f & y in dom f holds
ex p being Permutation of (dom f) st (f +* (x,(f . y))) +* (y,(f . x)) = f * p

proof end;

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

proof end;

:: from SCMBISORT, 2007.07.26, A.T.

theorem :: FUNCT_7:113

for f, g being FinSequence of INT
for m, n being Nat st 1 <= n & n <= len f & 1 <= m & m <= len f & g = (f +* (m,(f /. n))) +* (n,(f /. m)) holds
( f . m = g . n & f . n = g . m & ( for k being set st k <> m & k <> n & k in dom f holds
f . k = g . k ) & f,g are_fiberwise_equipotent )

proof end;

:: from SCMFSA10, 2007.07.27, A.T.

theorem :: FUNCT_7:114

for f being Function
for a, A, b, B, c, C being set st a <> b & a <> c holds
(((f +* (a .--> A)) +* (b .--> B)) +* (c .--> C)) . a = A

proof end;

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

theorem Th114: :: 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

proof end;

:: missing, 2008.03.23, A.T.

theorem Th115: :: FUNCT_7:116

for A being set
for f being Function
for x, y being object st rng f c= A holds
f +~ (x,y) = ((id A) +* (x,y)) * f

proof end;

theorem :: FUNCT_7:117

for f, g being Function
for x, y being object 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 Th117: :: FUNCT_7:118

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 Th118: :: FUNCT_7:119

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

proof end;

theorem Th119: :: FUNCT_7:120

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

proof end;

:: 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 & (a,b) followed_by c is Relation-like ) ;

end;

theorem Th120: :: FUNCT_7:121

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

proof end;

theorem Th121: :: FUNCT_7:122

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

proof end;

theorem Th122: :: FUNCT_7:123

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

proof end;

theorem Th123: :: FUNCT_7:124

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

proof end;

theorem Th124: :: FUNCT_7:125

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 Th125: :: FUNCT_7:126

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

proof end;

theorem :: FUNCT_7:127

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

proof end;

:: from POLYNOM1, 2008.12.15, A.T.

definition

let A, B be set ;
let f be Function of A,B;
let x be set ;
let y be Element of B;
:: original: +*
redefine func f +* (x,y) -> Function of A,B;
coherence
f +* (x,y) is Function of A,B

proof end;

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

proof end;

theorem :: FUNCT_7:129

for A, B being non empty set
for f, g being Function of A,B
for x being Element of A st ( for y being Element of A st f . y <> g . y holds
y = x ) holds
f = g +* (x,(f . x))

proof end;

theorem Th129: :: FUNCT_7:130

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:131

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

proof end;

theorem :: FUNCT_7:132

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:133

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

proof end;

theorem Th133: :: FUNCT_7:134

for A, B being set
for f, g being Function st dom f = dom g & dom f c= A \/ B & f | B = g | B holds
f,g equal_outside A by RELAT_1:153, XBOOLE_1:43;

theorem Th134: :: FUNCT_7:135

for A, B 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 by RELAT_1:153, XBOOLE_1:86;

theorem :: FUNCT_7:136

for A, B, I 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:137

for A, B, I 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 object ;
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:138

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

proof end;

theorem :: FUNCT_7:139

for I being non empty set
for X being ManySortedSet of I
for l1, l2 being Element of I
for i1, i2 being set holds X +* ((l1,l2) --> (i1,i2)) = (X +* (l1,i1)) +* (l2,i2)

proof end;

scheme :: FUNCT_7:sch 7
Unionx{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃() -> Element of F₁(), F₄() -> F₁() -valued Function, F₅() -> object , F₆( object ) -> object } :

{ F₆(i) where i is Element of F₁() : i in rng F₄() } = { F₆(j) where j is Element of F₁() : j in rng (F₄() +* (F₅(),F₂())) }

provided

A1: F₆(F₃()) = F₆(F₂()) and
A2: F₃() = F₄() . F₅()

proof end;