:: Miscellaneous Facts about Functions
::  by Grzegorz Bancerek and Andrzej Trybulec
::
:: Received January 12, 1996
:: Copyright (c) 1996-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, FUNCT_1, RELAT_1, TARSKI, XBOOLE_0, FUNCOP_1,
      PBOOLE, ZFMISC_1, FUNCT_4, FINSEQ_1, ARYTM_3, CARD_1, NAT_1, XXREAL_0,
      FINSET_1, SETFAM_1, FINSEQ_2, ORDINAL4, MCART_1, PARTFUN1, REWRITE1,
      FUNCT_2, ARYTM_1, RFINSEQ, CLASSES1, FUNCT_7, VALUED_1, ORDINAL1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, ENUMSET1, XTUPLE_0, SUBSET_1, CARD_1,
      WELLORD2, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, SETFAM_1, PBOOLE,
      DOMAIN_1, RELAT_1, FUNCT_1, RELSET_1, BINOP_1, FINSET_1, PARTFUN1,
      FUNCOP_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FUNCT_4, CLASSES1, RFINSEQ, NAT_D,
      REWRITE1, VALUED_1;
 constructors SETFAM_1, PARTFUN1, WELLORD2, BINOP_1, DOMAIN_1, FUNCT_4,
      XXREAL_0, NAT_1, INT_1, PBOOLE, RFINSEQ, NAT_D, REWRITE1, RELAT_2,
      REAL_1, CLASSES1, RELSET_1, VALUED_1, FINSEQ_2, XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, PARTFUN1,
      FUNCOP_1, FUNCT_4, XREAL_0, NAT_1, INT_1, CARD_1, FINSEQ_1, FUNCT_2,
      RELSET_1, XXREAL_0, XTUPLE_0, FINSEQ_3;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin :: Preliminaries

reserve a,x,y for object, A,B for set,
  l,m,n for Nat;

theorem :: FUNCT_7:1
  for f being Function, X being set st rng f c= X holds (id X)*f = f;

theorem :: FUNCT_7:2
  for X being set, Y being non empty set, f being Function of X,Y st f
is one-to-one for B being Subset of X, C being Subset of Y st C c= f.:B holds f
  "C c= B;

theorem :: FUNCT_7:3
  for X,Y be non empty set, f being Function of X,Y st f is
one-to-one for x being Element of X, A being Subset of X st f.x in f.:A holds x
  in A;

theorem :: FUNCT_7:4
  for X,Y be non empty set, f being Function of X,Y st f is
  one-to-one for x being Element of X, A being Subset of X, B being Subset of Y
  st f.x in f.:A \ B holds x in A \ f"B;

theorem :: FUNCT_7:5
  for X,Y be non empty set, f being Function of X,Y st f is one-to-one
for y being Element of Y, A being Subset of X, B being Subset of Y st y in f.:A
  \ B holds f".y in A \ f"B;

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

registration
  let x,y be object;
  cluster x .--> y -> non empty;
end;

registration
  let x,y,a,b be object;
  cluster (x,y) --> (a,b) -> non empty;
end;

theorem :: FUNCT_7:7
  for I being set, M being ManySortedSet of I for i being set st i
  in I holds i.--> (M.i) = M|{i};

theorem :: FUNCT_7:8
  for I,J being set, 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}:] qua set);

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

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

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

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

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

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

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

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

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

theorem :: FUNCT_7:18
 for x being object holds  <*x*> in A* iff x in A;

theorem :: FUNCT_7:19
  A* c= B* implies A c= B;

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

theorem :: FUNCT_7:21
  for A being finite set, X being non empty Subset-Family of A ex C
  being Element of X st for B being Element of X holds B c= C implies B = C;

theorem :: FUNCT_7:22
  for p,q being FinSequence st len p = len q+1
  for i being Nat holds i in dom q iff i in dom p & i+1 in dom p;

registration
  cluster Function-yielding non empty non-empty for FinSequence;
end;

registration
  cluster empty -> Function-yielding for Function;
end;

registration
  let n be Nat, f be Function;
  cluster n |-> f -> Function-yielding;
end;

registration
  let p,q be Function-yielding FinSequence;
  cluster p^q -> Function-yielding;
end;

theorem :: FUNCT_7:23
  for p,q being FinSequence st p^q is Function-yielding holds p is
  Function-yielding & q is Function-yielding;

begin :: Some useful schemes

scheme :: FUNCT_7:sch 1
  Kappa2D{ X,Y,Z()->non empty set,F(Element of X(),Element of Y())->object}:
  ex f being Function of [:X(),Y():], Z() st
  for x being Element of X(), y being Element of Y() holds f.(x,y)=F(x,y)
provided
 for x being Element of X(), y being Element of Y() holds F(x,y) in Z
();

scheme :: FUNCT_7:sch 2
  FinMono{ A() -> set, D() -> non empty set, F,G(object) -> object }:
  { F(d) where d
  is Element of D() : G(d) in A() } is finite
provided
 A() is finite and
 for d1,d2 being Element of D() st G(d1) = G(d2) holds d1 = d2;

scheme :: FUNCT_7:sch 3
  CardMono{ A() -> set, D() -> non empty set, G(object) -> object }:
  A(),{ d where d is Element of D() : G(d) in A() } are_equipotent
provided
 for x being set st x in A() ex d being Element of D() st x = G(d) and
 for d1,d2 being Element of D() st G(d1) = G(d2) holds d1 = d2;

scheme :: FUNCT_7:sch 4
  CardMono9{ A() -> set, D() -> non empty set, G(object) -> object }:
  A(),{ G(d)  where d is Element of D() : d in A() } are_equipotent
provided
 A() c= D() and
 for d1,d2 being Element of D() st G(d1) = G(d2) holds d1 = d2;

scheme :: FUNCT_7:sch 5
  FuncSeqInd {P[object]}: for p being Function-yielding FinSequence holds P[p]
provided
 P[ {} ] and
 for p being Function-yielding FinSequence st P[p] for f being
Function holds P[p^<*f*>];

begin :: Some auxiliary concepts

definition
::$CD
  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;

::$CT

theorem :: FUNCT_7:25
  for f be Function, A be set holds f,f equal_outside A;

theorem :: FUNCT_7:26
  for f,g be Function, A be set st f,g equal_outside A holds g,f
  equal_outside A;

theorem :: FUNCT_7:27
  for f,g,h be Function, A be set st f,g equal_outside A & g,h
  equal_outside A holds f,h equal_outside A;

theorem :: FUNCT_7:28
  for f,g be Function, A be set st f,g equal_outside A holds dom f
  \ A = dom g \ A;

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

definition
  let f be Function, i, x be object;
  func f+*(i,x) -> Function equals
:: FUNCT_7:def 3

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

theorem :: FUNCT_7:30
  for f be Function, d,i be object holds dom(f+*(i,d)) = dom f;

registration
 let f be empty Function, i, x be object;
 cluster f+*(i,x) -> empty;
end;

registration
 let f be non empty Function, i, x be object;
 cluster f+*(i,x) -> non empty;
end;

theorem :: FUNCT_7:31
  for f be Function, d,i be object st i in dom f holds (f+*(i,d)).i = d;

theorem :: FUNCT_7:32
  for f be Function, d,i,j be object st i <> j holds (f+*(i,d)).j = f.j;

theorem :: FUNCT_7:33
  for f be Function, d,e,i,j be set st i <> j holds f+*(i,d)+*(j,e) = f
  +*(j,e)+*(i,d);

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

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

registration
  let f be FinSequence, i,x be object;
  cluster f+*(i,x) -> FinSequence-like;
end;

definition
  let D be set, f be FinSequence of D, i be Nat, d be Element of D;
  redefine func f+*(i,d) -> FinSequence of D;
end;

theorem :: FUNCT_7:36
  for D be non empty set, f be FinSequence of D, d be Element of D, i be
  Nat st i in dom f holds (f+*(i,d))/.i = d;

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

theorem :: FUNCT_7:38
  for D be non empty set, f be FinSequence of D, d,e be Element of D, i
  be Nat holds f+*(i,f/.i) = f;

begin :: On the composition of a finite sequence of functions

definition
  let X be set;
  let p be Function-yielding FinSequence;
  func compose(p,X) -> Function means
:: 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
  for g,h being Function st g = f.i & h = p.(i+1) holds f.(i+1) = h*g;
end;

definition
  let p be Function-yielding FinSequence;
  let x be object;
  func apply(p,x) -> FinSequence means
:: FUNCT_7:def 5

  len it = len p+1 & it.1 = x &
for i being Nat, f being Function st i in dom p & f = p.i holds it.(
  i+1) = f.(it.i);
end;

reserve X,Y for set, x for object,
  p,q for Function-yielding FinSequence,
  f,g,h for Function;

theorem :: FUNCT_7:39
  compose({},X) = id X;

theorem :: FUNCT_7:40
  apply({},x) = <*x*>;

theorem :: FUNCT_7:41
  compose(p^<*f*>,X) = f*compose(p,X);

theorem :: FUNCT_7:42
  apply(p^<*f*>,x) = apply(p,x)^<*f.(apply(p,x).(len p+1))*>;

theorem :: FUNCT_7:43
  compose(<*f*>^p,X) = compose(p,f.:X)*(f|X);

theorem :: FUNCT_7:44
  apply(<*f*>^p,x) = <*x*>^apply(p,f.x);

theorem :: FUNCT_7:45
  compose(<*f*>,X) = f*id X;

theorem :: FUNCT_7:46
  dom f c= X implies compose(<*f*>,X) = f;

theorem :: FUNCT_7:47
  apply(<*f*>,x) = <*x,f.x*>;

theorem :: FUNCT_7:48
  rng compose(p,X) c= Y implies compose(p^q,X) = compose(q,Y)*compose(p,
  X );

theorem :: FUNCT_7:49
  apply(p^q,x).(len (p^q)+1) = apply(q,apply(p,x).(len p+1)).(len
  q+1);

theorem :: FUNCT_7:50
  apply(p^q,x) = apply(p,x)$^apply(q,apply(p,x).(len p+1));

theorem :: FUNCT_7:51
  compose(<*f,g*>,X) = g*f*id X;

theorem :: FUNCT_7:52
  dom f c= X or dom(g*f) c= X implies compose(<*f,g*>,X) = g*f;

theorem :: FUNCT_7:53
  apply(<*f,g*>,x) = <*x,f.x,g.(f.x)*>;

theorem :: FUNCT_7:54
  compose(<*f,g,h*>,X) = h*g*f*id X;

theorem :: FUNCT_7:55
  dom f c= X or dom(g*f) c= X or dom(h*g*f) c= X implies compose(<*f,g,h
  *>,X) = h*g*f;

theorem :: FUNCT_7:56
  apply(<*f,g,h*>,x) = <*x*>^<*f.x,g.(f.x),h.(g.(f.x))*>;

definition
  let F be FinSequence;
  func firstdom F -> set means
:: FUNCT_7:def 6

  it is empty if F is empty otherwise it = proj1
  (F.1);
  func lastrng F -> set means
:: FUNCT_7:def 7

  it is empty if F is empty otherwise it = proj2
  (F.len F);
end;

theorem :: FUNCT_7:57
  firstdom {} = {} & lastrng {} = {};

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

theorem :: FUNCT_7:59
  for p being Function-yielding FinSequence st p <> {} holds rng
  compose(p,X) c= lastrng p;

definition
  let IT be FinSequence;
  attr IT is FuncSeq-like means
:: 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;

theorem :: FUNCT_7:60
  for p,q being FinSequence st p^q is FuncSeq-like holds p is
  FuncSeq-like & q is FuncSeq-like;

registration
  cluster FuncSeq-like -> Function-yielding for FinSequence;
end;

registration
  cluster empty -> FuncSeq-like for FinSequence;
end;

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

registration
  cluster FuncSeq-like non empty non-empty for FinSequence;
end;

definition
  mode FuncSequence is FuncSeq-like FinSequence;
end;

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

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

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

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

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

definition
  let X,Y be set such that
 Y is empty implies X is empty;
  mode FuncSequence of X,Y -> FuncSequence means
:: FUNCT_7:def 9

    firstdom it = X &
    lastrng it c= Y;
end;

definition
  let Y be non empty set, X be set;
  let F be FuncSequence of X,Y;
  redefine func compose(F,X) -> Function of X,Y;
end;

definition
  let q be non-empty non empty FinSequence;
  mode FuncSequence of q -> FinSequence means
:: 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));
end;

registration
  let q be non-empty non empty FinSequence;
  cluster -> FuncSeq-like non-empty for FuncSequence of q;
end;

theorem :: FUNCT_7:66
  for q being non-empty non empty FinSequence, p being
  FuncSequence of q st p <> {} holds firstdom p = q.1 & lastrng p c= q.len q;

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

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

definition
  let f be Relation;
  let n be Nat;
  func iter (f,n) -> Relation means
:: 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);
end;

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

reserve m,n,k for Nat, R for Relation;

theorem :: FUNCT_7:68
  iter (R,0) = id(field R);

theorem :: FUNCT_7:69
  for n be Nat holds iter(R,n+1) = R*iter(R,n);

theorem :: FUNCT_7:70
  iter(R,1) = R;

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

theorem :: FUNCT_7:72
  dom iter(R,n) c= field R & rng iter(R,n) c= field R;

theorem :: FUNCT_7:73
  n <> 0 implies dom iter(R,n) c= dom R & rng iter(R,n) c= rng R;

theorem :: FUNCT_7:74
  for n being Nat st rng R c= dom R holds dom iter(R,n) = dom R &
  rng iter(R,n) c= dom R;

theorem :: FUNCT_7:75
  id(field R)*iter(R,n) = iter(R,n);

theorem :: FUNCT_7:76
  iter(R,n)*id(field R) = iter(R,n);

theorem :: FUNCT_7:77
  iter(R,m)*iter(R,n) = iter(R,n+m);

theorem :: FUNCT_7:78
  n <> 0 implies iter(iter(R,m),n) = iter(R,m*n);

theorem :: FUNCT_7:79
  rng R c= dom R implies iter(iter(R,m),n) = iter(R,m*n);

theorem :: FUNCT_7:80
  iter({},n) = {};

theorem :: FUNCT_7:81
  iter(id(X),n) = id(X);

theorem :: FUNCT_7:82
  rng R misses dom R implies iter(R,2) = {};

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

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

theorem :: FUNCT_7:85
  for f being Function of X,X holds iter(iter(f,m),n) = iter(f,m*n);

theorem :: FUNCT_7:86
  for f being PartFunc of X,X holds iter(f,n) is PartFunc of X,X;

theorem :: FUNCT_7:87
  n <> 0 & a in X & f = X --> a implies iter(f,n) = f;

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

begin :: Addenda

:: from SCMFSA6A, 2006.03.14, A.T.

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

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

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

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

theorem :: FUNCT_7:93
  for f,g being Function, a,b be object,
     A being set st f|A = g|A holds (f+*(a,b))|
  A = (g+*(a,b))|A;

:: from YELLOW14, 2006.03.14, A.T.

theorem :: FUNCT_7:94
  for f being Function, a, b being object holds (f +* (a .--> b)).a =
  b;

:: from SCMFSA6A, 2006.03.14, A.T.

theorem :: FUNCT_7:95
  for a, b being set holds <*a*> +* (1,b) = <*b*>;

:: from SCMFSA8C, 2006.03.15

theorem :: FUNCT_7:96
  for f be Function, x be set st x in dom f holds f +* (x .--> f.x) = f;

:: from JORDAN2B, 2007.03.18, A.T.

reserve i,j for Nat;

theorem :: FUNCT_7:97
  for w being FinSequence,r being object,i being natural Number
  holds len (w+*(i,r))=len w;

theorem :: FUNCT_7:98
  for D being non empty set, w being FinSequence of D, r being Element
  of D st i in dom w holds w+*(i,r)=(w|(i-'1))^<*r*>^(w/^i);

:: comp. FINSEQ_7, 2007.03.18, A.T.

reserve F for Function,
  e,x,y,z for object;

definition
  let F;
  let x,y be object;
  func Swap(F,x,y) -> set equals
:: FUNCT_7:def 12

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

registration
  let F;
  let x,y be object;
  cluster Swap(F,x,y) -> Relation-like Function-like;
end;

theorem :: FUNCT_7:99
 for x,y being object holds dom Swap(F,x,y) = dom F;

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

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

theorem :: FUNCT_7:102
  x in dom F implies y in rng(F+*(x,y));

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

:: from SCMFSA_7, 2007.07.22, A.T.

scheme :: FUNCT_7:sch 6
  { A() -> set, D() -> non empty set, G(object) -> object }:
  A(),{ G(d) where d is Element of D() : d in A() } are_equipotent
provided
 A() c= D() and
 for d1,d2 being Element of D() st d1 in A() & d2 in A() & G(d1) = G(
d2) holds d1 = d2;

:: from SCMFSA6A, 2007.07.23, A.T.

theorem :: FUNCT_7:104
  for f,g,h being Function, A being set holds f, g equal_outside A
  implies f +* h, g +* h equal_outside A;

theorem :: FUNCT_7:105
  for f,g,h being Function, A being set holds f, g equal_outside A
  implies h +* f, h +* g equal_outside A;

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

:: from SF_MASTR, 2007.07.25, A.T.

theorem :: FUNCT_7:107
  for x, y, a being object, f being Function st f.x = f.y holds f.a
  = (f*((id dom f)+*(x,y))).a;

theorem :: FUNCT_7:108
  for x, y being set, 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));

::$CT

:: from SFMASTR3, 2007.07.26, A.T.

theorem :: FUNCT_7:110
  for X being set, p being Permutation of X, x, y being Element
  of X holds p+*(x, p.y)+*(y, p.x) is Permutation of X;

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

:: from SCMISORT, 2007.07.26, A.T.

theorem :: FUNCT_7:112
  for f be Function,d,r be set st d in dom f holds dom f=dom (f+*(d.-->r
  ));

:: from SCMBISORT, 2007.07.26, A.T.

theorem :: FUNCT_7:113
  for f,g be FinSequence of INT,m,n be 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 be set st k<>m & k<>n & k in dom f holds f.k=g.k) & f,g
  are_fiberwise_equipotent;

:: from SCMFSA10, 2007.07.27, A.T.

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

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

theorem :: FUNCT_7:115
  for A, B, a, b being set, f being Function of A,B st b in B
  holds f +* (a,b) is Function of A,B;

:: missing, 2008.03.23, A.T.

theorem :: FUNCT_7:116
  rng f c= A implies f+~(x,y) = (id A+*(x,y))*f;

theorem :: FUNCT_7:117
  (f+*g)+~(x,y) = f+~(x,y)+*(g+~(x,y));

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

registration
  let a,b be set;
  cluster a followed_by b -> Function-like Relation-like;
end;

reserve a,b,c for set;

theorem :: FUNCT_7:118
  dom(a followed_by b) = NAT;

definition
  let X be non empty set;
  let a,b be Element of X;
  redefine func a followed_by b -> sequence of X;
end;

theorem :: FUNCT_7:119
  (a followed_by b).0 = a;

theorem :: FUNCT_7:120
  for n st n > 0 holds (a followed_by b).n = b;

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

registration
  let a,b,c be set;
  cluster (a,b) followed_by c -> Function-like Relation-like;
end;

theorem :: FUNCT_7:121
  dom (a,b) followed_by c = NAT;

theorem :: FUNCT_7:122
  ((a,b) followed_by c).0 = a;

theorem :: FUNCT_7:123
  ((a,b) followed_by c).1 = b;

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

theorem :: FUNCT_7:125
  (a,b) followed_by c = (a followed_by c) +* (1,b);

definition
  let X be non empty set;
  let a,b,c be Element of X;
  redefine func (a,b) followed_by c -> sequence of X;
end;

theorem :: FUNCT_7:126
  rng(a followed_by b) = {a,b};

theorem :: FUNCT_7:127
  rng (a,b) followed_by c = {a,b,c};

:: from POLYNOM1, 2008.12.15, A.T.

definition
  let A, B be set, f be Function of A, B, x be set, y be Element of B;
  redefine func f+*(x,y) -> Function of A, B;
end;

:: missing, 2008.12.14, A.T.

theorem :: FUNCT_7:128
  for A, B being non empty set, f being Function of A, B, x being
  Element of A, y being set holds f+*(x,y).x = y;

theorem :: FUNCT_7:129
  for A, B being non empty set, f,g being Function of A, B, 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);

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

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

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

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

theorem :: FUNCT_7:134
 dom f = dom g & dom f c= A \/ B & f|B = g|B
  implies f,g equal_outside A;

theorem :: FUNCT_7:135
 dom f = dom g & B c= dom f & A misses B & f,g equal_outside A
  implies f|B = g|B;

reserve A,B,I for set, X,Y for ManySortedSet of I;

theorem :: FUNCT_7:136
 I c= A \/ B & X|B = Y|B implies X,Y equal_outside A;

theorem :: FUNCT_7:137
 B c= I & A misses B & X,Y equal_outside A implies X|B = Y|B;

registration let V be non empty set;
 let f be V-valued Function, x be object, y be Element of V;
 cluster f+*(x,y) -> V-valued;
end;

theorem :: FUNCT_7:138
 f c= g & not x in dom f implies f c= g+*(x,y);

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

scheme :: FUNCT_7:sch 7
 Unionx { A()-> non empty set, a,b()-> Element of A(),
   f() -> A()-valued Function,
   x() -> object, F(object) -> object }:
  { F(i) where i is Element of A() : i in rng f()} =
    { F(j) where j is Element of A() : j in rng(f()+*(x(),a()))}
 provided
 F(b()) = F(a()) and
 b() = f().x();