The abstract of the Mizar article:

The Modification of a Function by a Function and the Iteration of the Composition of a Function

by

Czeslaw Bylinski

Received March 1, 1990

MML identifier: FUNCT_4

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_1, TARSKI, RELAT_1, BOOLE, FUNCOP_1, PARTFUN1, FUNCT_2,
      FUNCT_4;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
      FUNCT_2, PARTFUN1, FUNCOP_1;
 constructors PARTFUN1, FUNCOP_1, TARSKI, XBOOLE_0;
 clusters RELAT_1, FUNCT_1, RELSET_1, XBOOLE_0, FUNCOP_1, ZFMISC_1;
 requirements BOOLE, SUBSET;


begin

 reserve a,b,p,x,x',x1,x1',x2,y,y',y1,y1',y2,z,z',z1,z2,X,X',Y,Y',Z,Z'
   for set;
 reserve A,D,D' for non empty set;
 reserve f,g,h for Function;

theorem :: FUNCT_4:1
   (for z st z in Z holds ex x,y st z = [x,y]) implies ex X,Y st Z c= [:X,Y:];

theorem :: FUNCT_4:2
     g*f = (g|rng f)*f;

theorem :: FUNCT_4:3
     {} = {} --> a;

theorem :: FUNCT_4:4
     id X c= id Y iff X c= Y;

theorem :: FUNCT_4:5
     X c= Y implies X --> a c= Y --> a;

theorem :: FUNCT_4:6
   X --> a c= Y --> b implies X c= Y;

theorem :: FUNCT_4:7
     X <> {} & X --> a c= Y --> b implies a = b;

theorem :: FUNCT_4:8
     x in dom f implies {x} --> f.x c= f;

:: Natural order on functions

definition let f,g;
 redefine pred f c= g;
  synonym f <= g;
end;

theorem :: FUNCT_4:9
     Y|f|X <= f;

theorem :: FUNCT_4:10
     f <= g implies Y|f|X <= Y|g|X;

definition let f,g;
  func f +* g -> Function means
:: FUNCT_4:def 1
  dom it = dom f \/ dom g &
  for x st x in dom f \/ dom g
   holds (x in dom g implies it.x = g.x) & (not x in dom g implies it.x = f.x);
  idempotence;
end;

theorem :: FUNCT_4:11
     dom f c= dom(f+*g) & dom g c= dom(f+*g);

theorem :: FUNCT_4:12
   not x in dom g implies (f +* g).x = f.x;

theorem :: FUNCT_4:13
   x in dom(f +* g) iff x in dom f or x in dom g;

theorem :: FUNCT_4:14
   x in dom g implies (f+*g).x = g.x;

theorem :: FUNCT_4:15
     f +* g +* h = f +* (g +* h);

theorem :: FUNCT_4:16
   f tolerates g & x in dom f implies (f+*g).x = f.x;

theorem :: FUNCT_4:17
     dom f misses dom g & x in dom f implies (f +* g).x = f.x;

theorem :: FUNCT_4:18
   rng(f +* g) c= rng f \/ rng g;

theorem :: FUNCT_4:19
     rng g c= rng(f +* g);

theorem :: FUNCT_4:20
   dom f c= dom g implies f +* g = g;

theorem :: FUNCT_4:21
     {} +* f = f;

theorem :: FUNCT_4:22
     f +* {} = f;

theorem :: FUNCT_4:23
     id(X) +* id(Y) = id(X \/ Y);

theorem :: FUNCT_4:24
     (f +* g)|(dom g) = g;

theorem :: FUNCT_4:25
   ((f +* g)|(dom f \ dom g)) c= f;

theorem :: FUNCT_4:26
    g c= (f +* g);

theorem :: FUNCT_4:27
     f tolerates g +* h implies f|(dom f \ dom h) tolerates g;

theorem :: FUNCT_4:28
   f tolerates g +* h implies f tolerates h;

theorem :: FUNCT_4:29
   f tolerates g iff f c= f +* g;

theorem :: FUNCT_4:30
   f +* g c= f \/ g;

theorem :: FUNCT_4:31
   f tolerates g iff f \/ g = f +* g;

theorem :: FUNCT_4:32
   dom f misses dom g implies f \/ g = f +* g;

theorem :: FUNCT_4:33
     dom f misses dom g implies f c= f +* g;

theorem :: FUNCT_4:34
     dom f misses dom g implies (f +* g)|(dom f) = f;

theorem :: FUNCT_4:35
   f tolerates g iff f +* g = g +* f;

theorem :: FUNCT_4:36
     dom f misses dom g implies f +* g = g +* f;

theorem :: FUNCT_4:37
     for f,g being PartFunc of X,Y st g is total holds f +* g = g;

theorem :: FUNCT_4:38
   for f,g being Function of X,Y st Y = {} implies X = {} holds f +* g = g;

theorem :: FUNCT_4:39
     for f,g being Function of X,X holds f +* g = g;

theorem :: FUNCT_4:40
     for f,g being Function of X,D holds f +* g = g;

theorem :: FUNCT_4:41
     for f,g being PartFunc of X,Y holds f +* g is PartFunc of X,Y;

:: The converse function whenever domain

definition let f;
 func ~f -> Function means
:: FUNCT_4:def 2
  (for x holds x in dom it iff ex y,z st x = [z,y] & [y,z] in dom f) &
  (for y,z st [y,z] in dom f holds it.[z,y] = f.[y,z]);
end;

theorem :: FUNCT_4:42
   rng ~f c= rng f;

theorem :: FUNCT_4:43
   [x,y] in dom f iff [y,x] in dom ~f;

theorem :: FUNCT_4:44
     [y,x] in dom ~f implies (~f).[y,x] = f.[x,y];

theorem :: FUNCT_4:45
     ex X,Y st dom ~f c= [:X,Y:];

theorem :: FUNCT_4:46
   dom f c= [:X,Y:] implies dom ~f c= [:Y,X:];

theorem :: FUNCT_4:47
   dom f = [:X,Y:] implies dom ~f = [:Y,X:];

theorem :: FUNCT_4:48
   dom f c= [:X,Y:] implies rng ~f = rng f;

theorem :: FUNCT_4:49
     for f being PartFunc of [:X,Y:],Z holds ~f is PartFunc of [:Y,X:],Z;

theorem :: FUNCT_4:50
   for f being Function of [:X,Y:],Z st Z<>{} holds ~f is Function of [:Y,X:],Z
;

theorem :: FUNCT_4:51
     for f being Function of [:X,Y:],D holds ~f is Function of [:Y,X:],D
;

theorem :: FUNCT_4:52
    ~~f c= f;

theorem :: FUNCT_4:53
   dom f c= [:X,Y:] implies ~~f = f;

theorem :: FUNCT_4:54
     for f being PartFunc of [:X,Y:],Z holds ~~f = f;

theorem :: FUNCT_4:55
   for f being Function of [:X,Y:],Z st Z <> {} holds ~~f = f;

theorem :: FUNCT_4:56
     for f being Function of [:X,Y:],D holds ~~f = f;

:: Product of 2'ary functions

definition let f,g;
  func |:f,g:| -> Function means
:: FUNCT_4:def 3

  (for z holds z in dom it iff
    ex x,y,x',y' st z = [[x,x'],[y,y']] & [x,y] in dom f & [x',y'] in dom g) &
  (for x,y,x',y' st [x,y] in dom f & [x',y'] in dom g
     holds it.[[x,x'],[y,y']] = [f.[x,y],g.[x',y']]);
end;

theorem :: FUNCT_4:57
   [[x,x'],[y,y']] in dom |:f,g:| iff [x,y] in dom f & [x',y'] in dom g;

theorem :: FUNCT_4:58
     [[x,x'],[y,y']] in dom |:f,g:|
     implies |:f,g:|.[[x,x'],[y,y']] = [f.[x,y],g.[x',y']];

theorem :: FUNCT_4:59
   rng |:f,g:| c= [:rng f,rng g:];

theorem :: FUNCT_4:60
   dom f c= [:X,Y:] & dom g c= [:X',Y':]
     implies dom|:f,g:| c= [:[:X,X':],[:Y,Y':]:];

theorem :: FUNCT_4:61
   dom f = [:X,Y:] & dom g = [:X',Y':]
     implies dom|:f,g:| = [:[:X,X':],[:Y,Y':]:];

theorem :: FUNCT_4:62
     for f being PartFunc of [:X,Y:],Z for g being PartFunc of [:X',Y':],Z'
    holds |:f,g:| is PartFunc of [:[:X,X':],[:Y,Y':]:],[:Z,Z':];

theorem :: FUNCT_4:63
   for f being Function of [:X,Y:],Z for g being Function of [:X',Y':],Z'
     st Z <> {} & Z' <> {}
    holds |:f,g:| is Function of [:[:X,X':],[:Y,Y':]:],[:Z,Z':];

theorem :: FUNCT_4:64
     for f being Function of [:X,Y:],D for g being Function of [:X',Y':],D'
    holds |:f,g:| is Function of [:[:X,X':],[:Y,Y':]:],[:D,D':];

definition let x,y,a,b be set;
  func (x,y) --> (a,b) -> set equals
:: FUNCT_4:def 4
   ({x} --> a) +* ({y} --> b);
end;

definition let x,y,a,b be set;
  cluster (x,y) --> (a,b) -> Function-like Relation-like;
end;

theorem :: FUNCT_4:65
  dom((x1,x2) --> (y1,y2)) = {x1,x2} & rng((x1,x2) --> (y1,y2)) c= {y1,y2};

theorem :: FUNCT_4:66
  x1 <> x2 implies
    ((x1,x2) --> (y1,y2)).x1 = y1 & ((x1,x2) --> (y1,y2)).x2 = y2;

theorem :: FUNCT_4:67
    x1 <> x2 implies rng((x1,x2) --> (y1,y2)) = {y1,y2};

theorem :: FUNCT_4:68
    (x1,x2) --> (y,y) = {x1,x2} --> y;

definition let A,x1,x2; let y1,y2 be Element of A;
  redefine func (x1,x2) --> (y1,y2) -> Function of {x1,x2},A;
end;

theorem :: FUNCT_4:69
   for a,b,c,d being set,
     g being Function st dom g = {a,b} & g.a = c & g.b = d holds
   g = (a,b) --> (c,d);

theorem :: FUNCT_4:70
 for x,y being set holds {x} --> y = {[x,y]};

theorem :: FUNCT_4:71
   for a,b,c,d being set st a <> c
  holds (a,c) --> (b,d) = { [a,b], [c,d] };

theorem :: FUNCT_4:72
   for a,b,x,y,x',y' being set
  st a <> b & (a,b) --> (x,y) = (a,b) --> (x',y')
  holds x = x' & y = y';