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

Copyright (c) 1990 Association of Mizar Users

MML identifier: FUNCT_4
[ 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;
 definitions TARSKI, FUNCT_2, PARTFUN1, XBOOLE_0;
 theorems TARSKI, FUNCT_1, FUNCT_2, GRFUNC_1, PARTFUN1, FUNCOP_1, ZFMISC_1,
      RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, ENUMSET1;
 schemes FUNCT_1, PARTFUN1, XBOOLE_0;

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;

:: Auxiliary theorems

Lm1: [x,y] in Z implies x in union union Z & y in union union Z
 proof assume
A1:  [x,y] in Z;
  set xy=[x,y];
    [x,y] = { {x,y}, {x} } by TARSKI:def 5;
  then {x,y} in xy & {x} in xy by TARSKI:def 2;
then A2:  {x,y} in union Z & {x} in union Z by A1,TARSKI:def 4;
    y in {x,y} & x in {x} by TARSKI:def 1,def 2;
  hence thesis by A2,TARSKI:def 4; end;

Lm2: [[x,x'],[y,y']] = [[x1,x1'],[y1,y1']]
      implies x = x1 & y = y1 & x'= x1' & y' = y1'
 proof assume [[x,x'],[y,y']] = [[x1,x1'],[y1,y1']];
  then [x,x'] = [x1,x1'] & [y,y'] = [y1,y1'] by ZFMISC_1:33;
  hence thesis by ZFMISC_1:33;
 end;

theorem Th1:
   (for z st z in Z holds ex x,y st z = [x,y]) implies ex X,Y st Z c= [:X,Y:]
 proof assume
A1:  for z st z in Z holds ex x,y st z = [x,y];
   defpred P[set] means ex y st [$1,y] in Z;
   consider X such that
A2:  x in X iff x in union union Z & P[x] from Separation;
   defpred P[set] means ex x st [x,$1] in Z;
   consider Y such that
A3:  y in Y iff y in union union Z & P[y] from Separation;
  take X,Y;
  let z;
  assume
A4:  z in Z;
  then consider x,y such that
A5:  z = [x,y] by A1;
    y in union union Z & x in union union Z by A4,A5,Lm1;
  then y in Y & x in X by A2,A3,A4,A5;
  hence z in [:X,Y:] by A5,ZFMISC_1:106; end;

theorem
     g*f = (g|rng f)*f
 proof
    x in dom(g*f) iff x in dom((g|rng f)*f)
   proof
A1:    dom(g|rng f) = dom g /\ rng f by RELAT_1:90;
    thus x in dom(g*f) implies x in dom((g|rng f)*f)
     proof assume x in dom(g*f);
      then x in dom f & f.x in dom g by FUNCT_1:21;
      then x in dom f & f.x in dom g & f.x in rng f by FUNCT_1:def 5;
      then x in dom f & f.x in dom(g|rng f) by A1,XBOOLE_0:def 3;
      hence thesis by FUNCT_1:21;
     end;
    assume x in dom((g|rng f)*f);
    then x in dom f & f.x in dom(g|rng f) by FUNCT_1:21;
    then x in dom f & f.x in dom g by A1,XBOOLE_0:def 3;
    hence thesis by FUNCT_1:21;
   end;
then A2:  dom(g*f) = dom((g|rng f)*f) by TARSKI:2;
    x in dom(g*f) implies (g*f).x = ((g|rng f)*f).x
   proof assume
A3:    x in dom(g*f);
then A4:    x in dom f & f.x in dom g by FUNCT_1:21;
then A5:    f.x in rng f by FUNCT_1:def 5;
    thus (g*f).x = g.(f.x) by A3,FUNCT_1:22
                .= (g|rng f).(f.x) by A5,FUNCT_1:72
                .= ((g|rng f)*f).x by A4,FUNCT_1:23;
   end;
  hence thesis by A2,FUNCT_1:9; end;

theorem
     {} = {} --> a
 proof dom ({} --> a) = {} by FUNCOP_1:16; hence thesis by RELAT_1:64; end;

theorem
     id X c= id Y iff X c= Y
 proof
   thus id X c= id Y implies X c= Y
    proof assume
A1:     id X c= id Y;
     let x;
     assume x in X;
     then [x,x] in id X by RELAT_1:def 10;
     hence thesis by A1,RELAT_1:def 10;
    end;
   assume
A2:   X c= Y;
   let z; assume
A3:   z in id X;
   then consider x,x' such that
A4:   x in X and x' in X and
A5:   z = [x,x'] by ZFMISC_1:103;
     x in Y & x = x' by A2,A3,A4,A5,RELAT_1:def 10;
   hence z in id Y by A5,RELAT_1:def 10; end;

theorem
     X c= Y implies X --> a c= Y --> a
 proof assume
A1:  X c= Y;
A2:  dom(X --> a) = X & dom(Y --> a) = Y by FUNCOP_1:19;
    now let x;
   assume x in dom(X --> a);
   then (X --> a).x = a & (Y --> a).x = a by A1,A2,FUNCOP_1:13;
   hence (X --> a).x = (Y --> a).x;
  end;
  hence thesis by A1,A2,GRFUNC_1:8;
 end;

theorem Th6:
   X --> a c= Y --> b implies X c= Y
 proof assume X --> a c= Y --> b;
  then dom(X --> a) c= dom(Y --> b) & dom(X --> a) = X & dom(Y --> b) = Y
   by FUNCOP_1:19,RELAT_1:25;
  hence X c= Y; end;

theorem
     X <> {} & X --> a c= Y --> b implies a = b
 proof assume
A1: X <> {};
  consider x being Element of X;
  assume
A2:  X --> a c= Y --> b;
  then X c= Y by Th6;
  then x in Y & dom(X --> a) = X by A1,FUNCOP_1:19,TARSKI:def 3;
  then (X --> a).x = a & (Y --> b).x = b & (X --> a).x = (Y --> b).x
   by A1,A2,FUNCOP_1:13,GRFUNC_1:8;
  hence thesis; end;

theorem
     x in dom f implies {x} --> f.x c= f
 proof assume
A1:  x in dom f;
A2:  dom ({x} --> f.x) = {x} by FUNCOP_1:19;
A3:  dom ({x} --> f.x) c= dom f
      proof let y;
       assume y in dom ({x} --> f.x);
       hence thesis by A1,A2,TARSKI:def 1;
      end;
     now let y;
    assume y in dom ({x} --> f.x);
    then ({x} --> f.x).y = f.x & y = x by A2,FUNCOP_1:13,TARSKI:def 1;
    hence ({x} --> f.x).y = f.y;
   end;
  hence thesis by A3,GRFUNC_1:8; end;

:: Natural order on functions

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

theorem
     Y|f|X <= f
 proof Y|f|X <= Y|f & Y|f <= f by RELAT_1:88,117;
 hence thesis by XBOOLE_1:1; end;

theorem
     f <= g implies Y|f|X <= Y|g|X
 proof assume f <= g; then Y|f <=
 Y|g by RELAT_1:132; hence thesis by RELAT_1:105;
 end;

definition let f,g;
  func f +* g -> Function means
:Def1:  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);
 existence
 proof
   defpred P[set] means $1 in dom g;
   deffunc F(set) = g.$1;
   deffunc G(set) = f.$1;
   thus ex F being Function st dom F = dom f \/ dom g &
   for x st x in dom f \/ dom g holds (P[x] implies F.x = F(x)) &
   (not P[x] implies F.x = G(x)) from LambdaC;
 end;
 uniqueness
  proof let h1,h2 be Function such that
A1:  dom h1 = dom f \/ dom g and
A2:  for x st x in dom f \/ dom g holds
      (x in dom g implies h1.x = g.x) & (not x in dom g implies h1.x = f.x) and
A3:  dom h2 = dom f \/ dom g and
A4:  for x st x in dom f \/ dom g holds
      (x in dom g implies h2.x = g.x) & (not x in dom g implies h2.x = f.x);
     for x st x in dom f \/ dom g holds h1.x = h2.x
    proof let x;
     assume x in dom f \/ dom g;
     then (x in dom g implies h1.x = g.x & h2.x = g.x) &
      (not x in dom g implies h1.x = f.x & h2.x = f.x) by A2,A4;
     hence thesis;
    end;
   hence thesis by A1,A3,FUNCT_1:9;
  end;
  idempotence;
end;

theorem
     dom f c= dom(f+*g) & dom g c= dom(f+*g)
  proof dom(f+*g) = dom f \/ dom g by Def1;
   hence thesis by XBOOLE_1:7;
  end;

theorem Th12:
   not x in dom g implies (f +* g).x = f.x
 proof assume
A1: not x in dom g;
  per cases;
  suppose x in dom f;
   then x in dom f \/ dom g & not x in dom g by A1,XBOOLE_0:def 2;
  hence thesis by Def1;
  suppose
A2: not x in dom f;
   then not x in dom f \/ dom g by A1,XBOOLE_0:def 2;
   then not x in dom(f+*g) by Def1;
  hence (f+*g).x = {} by FUNCT_1:def 4
          .= f.x by A2,FUNCT_1:def 4;
 end;

theorem Th13:
   x in dom(f +* g) iff x in dom f or x in dom g
 proof x in dom(f +* g) iff x in dom f \/ dom g by Def1;
  hence thesis by XBOOLE_0:def 2; end;

theorem Th14:
   x in dom g implies (f+*g).x = g.x
 proof x in dom g implies x in dom f \/ dom g by XBOOLE_0:def 2;
  hence thesis by Def1; end;

theorem
     f +* g +* h = f +* (g +* h)
 proof
A1: dom(f +* g +* h) = dom(f +* g) \/ dom h by Def1
       .= dom f \/ dom g \/ dom h by Def1
       .= dom f \/ (dom g \/ dom h) by XBOOLE_1:4
       .= dom f \/ dom(g +* h) by Def1;
    now let x such that x in dom f \/ dom(g +* h);
   hereby assume
A2: x in dom(g +* h);
     per cases by A2,Th13;
    suppose
A3:   x in dom g & not x in dom h;
    hence (f +* g +* h).x = (f +* g).x by Th12
       .= g.x by A3,Th14
       .= (g +* h).x by A3,Th12;
    suppose
A4:   x in dom h;
    hence (f +* g +* h).x = h.x by Th14
     .= (g +* h).x by A4,Th14;
   end;
   assume not x in dom(g +* h);
then A5:   not x in dom g & not x in dom h by Th13;
   hence (f +* g +* h).x = (f +* g).x by Th12
       .= f.x by A5,Th12;
  end;
  hence thesis by A1,Def1;
 end;

theorem Th16:
   f tolerates g & x in dom f implies (f+*g).x = f.x
 proof assume that
A1:  f tolerates g and
A2:  x in dom f;
    now per cases;
   suppose x in dom g;
    then x in dom f /\ dom g & (f+*g).x = g.x by A2,Th14,XBOOLE_0:def 3;
    hence (f+*g).x = f.x by A1,PARTFUN1:def 6;
   suppose not x in dom g;
    hence (f+*g).x = f.x by Th12;
  end;
  hence thesis; end;

theorem
     dom f misses dom g & x in dom f implies (f +* g).x = f.x
 proof assume that
A1:  dom f /\ dom g = {} and
A2:  x in dom f;
     not x in dom g by A1,A2,XBOOLE_0:def 3;
  hence thesis by Th12; end;

theorem Th18:
   rng(f +* g) c= rng f \/ rng g
 proof let y;
  assume y in rng(f +* g);
  then consider x such that
A1: x in dom (f +* g) and
A2: y = (f +* g).x by FUNCT_1:def 5;
    x in dom f & not x in dom g or x in dom g by A1,Th13;
  then x in dom f & (f +* g).x = f.x or x in dom g & (f +* g).x = g.x
    by Th12,Th14;
  then y in rng f or y in rng g by A2,FUNCT_1:def 5;
  hence thesis by XBOOLE_0:def 2; end;

theorem
     rng g c= rng(f +* g)
 proof let y; assume y in rng g;
  then consider x such that
A1: x in dom g & y = g.x by FUNCT_1:def 5;
    x in dom(f +* g) & (f +* g).x = y by A1,Th13,Th14;
  hence thesis by FUNCT_1:def 5; end;

theorem Th20:
   dom f c= dom g implies f +* g = g
 proof assume dom f c= dom g;
  then dom f \/ dom g = dom g by XBOOLE_1:12;
  then dom(f +* g) = dom g & for x st x in dom g holds (f +* g).x = g.x
    by Def1;
  hence thesis by FUNCT_1:9; end;

theorem
     {} +* f = f
 proof dom {} c= dom f by XBOOLE_1:2; hence thesis by Th20; end;

theorem
     f +* {} = f
 proof dom f \/ dom {} = dom f;
then A1:  dom(f +* {}) = dom f by Def1;
    for x st x in dom f holds (f +* {}).x = f.x
   proof let x; assume x in dom f;
    then x in dom f \ dom {};
    hence thesis by Th12;
   end;
  hence thesis by A1,FUNCT_1:9; end;

theorem
     id(X) +* id(Y) = id(X \/ Y)
 proof
A1:  dom(id(X) +* id(Y)) = dom id X \/ dom id Y by Def1
                        .= X \/ dom id Y by RELAT_1:71
                        .= X \/ Y by RELAT_1:71
                        .= dom id(X \/ Y) by RELAT_1:71;
    x in dom id(X \/ Y) implies (id(X) +* id(Y)).x = id(X \/ Y).x
   proof assume
A2:   x in dom id(X \/ Y);
      now per cases;
     suppose
A3:    x in Y; dom id Y = Y by RELAT_1:71;
      hence (id(X) +* id(Y)).x = (id Y).x by A3,Th14
                              .= x by A3,FUNCT_1:35
                              .= id(X \/ Y).x by A2,FUNCT_1:35;
     suppose
A4:     not x in Y;
then A5:     x in X by A2,XBOOLE_0:def 2;
      then x in dom id X & not x in dom id Y by A4,RELAT_1:71;
      hence (id(X) +* id(Y)).x = (id X).x by Th12
                              .= x by A5,FUNCT_1:35
                              .= id(X \/ Y).x by A2,FUNCT_1:35;
    end;
    hence (id(X) +* id(Y)).x = id(X \/ Y).x;
   end;
  hence thesis by A1,FUNCT_1:9; end;

theorem
     (f +* g)|(dom g) = g
 proof dom f \/ dom g = dom(f +* g) by Def1;
  then dom g c= dom(f +* g) by XBOOLE_1:7;
then A1:  dom((f +* g)|(dom g)) = dom g by RELAT_1:91;
    for x st x in dom g holds ((f +* g)|(dom g)).x = g.x
   proof let x;
      x in dom g implies (f +* g).x = g.x by Th14;
    hence thesis by A1,FUNCT_1:70;
   end;
  hence thesis by A1,FUNCT_1:9; end;

theorem Th25:
   ((f +* g)|(dom f \ dom g)) c= f
 proof
    dom f \ dom g c= dom f & dom((f +* g)|(dom f \ dom g)) c= dom f \ dom g
   by RELAT_1:87,XBOOLE_1:36;
then A1:  dom((f +* g)|(dom f \ dom g)) c= dom f by XBOOLE_1:1;
    for x st x in dom((f +* g)|(dom f \ dom g))
   holds ((f +* g)|(dom f \ dom g)).x = f.x
   proof let x such that
A2:    x in dom((f +* g)|(dom f \ dom g));
      dom((f +* g)|(dom f \ dom g)) c= dom f \ dom g by RELAT_1:87;
    then not x in dom g by A2,XBOOLE_0:def 4;
    then (f +* g).x = f.x by Th12;
    hence thesis by A2,FUNCT_1:70;
   end;
  hence thesis by A1,GRFUNC_1:8; end;

theorem Th26:
    g c= (f +* g)
 proof dom(f +* g) = dom f \/ dom g by Def1;
  then dom g c= dom(f +* g) & for x st x in dom g holds (f+*g).x = g.x
   by Th14,XBOOLE_1:7;
  hence thesis by GRFUNC_1:8; end;

theorem
     f tolerates g +* h implies f|(dom f \ dom h) tolerates g
 proof assume
A1:  f tolerates g +* h;
  let x;
  assume x in dom(f|(dom f \ dom h)) /\ dom g;
then A2:  x in dom(f|(dom f \ dom h)) & x in dom g by XBOOLE_0:def 3;
A3:  dom(f|(dom f \ dom h)) c= dom f \ dom h by RELAT_1:87;
then A4: x in dom f & not x in dom h by A2,XBOOLE_0:def 4;
  then x in dom f & x in dom g \ dom h & x in
 dom(g +* h) by A2,Th13,XBOOLE_0:def 4;
  then x in dom f & (g +* h).x = g.x & x in dom f /\ dom(g +* h)
                  by A4,Th12,XBOOLE_0:def 3;
  then x in dom f & f.x = g.x by A1,PARTFUN1:def 6;
  hence (f|(dom f \ dom h)).x = g.x by A2,A3,FUNCT_1:72; end;

theorem Th28:
   f tolerates g +* h implies f tolerates h
 proof assume
A1:  f tolerates g +* h;
  let x; assume x in dom f /\ dom h;
  then x in dom f & x in dom h by XBOOLE_0:def 3;
  then x in dom f & x in dom(g +* h) & (g +* h).x = h.x by Th13,Th14;
  then x in dom f /\ dom(g +* h) & (g +* h).x = h.x by XBOOLE_0:def 3;
  hence f.x = h.x by A1,PARTFUN1:def 6; end;

theorem Th29:
   f tolerates g iff f c= f +* g
 proof
  thus f tolerates g implies f c= (f +* g)
   proof assume
A1: f tolerates g;
      dom f \/ dom g = dom(f +* g) by Def1;
    then dom f c= dom(f +* g) & (for x st x in dom f holds (f +* g).x = f.x)
      by A1,Th16,XBOOLE_1:7;
    hence thesis by GRFUNC_1:8;
   end;
  assume f c= (f +* g);
  then f tolerates f +* g by PARTFUN1:135;
  hence thesis by Th28; end;

theorem Th30:
   f +* g c= f \/ g
 proof let p; assume
A1:  p in f +* g;
  then consider x,y such that
A2:  p = [x,y] by RELAT_1:def 1;
    x in dom(f +* g) & y = (f +* g).x by A1,A2,FUNCT_1:8;
  then x in dom f & not x in dom g or x in dom g by Th13;
  then y = (f +* g).x &
        (x in dom f & (f +* g).x = f.x or x in dom g & (f +* g).x = g.x)
   by A1,A2,Th12,Th14,FUNCT_1:8;
  then p in f or p in g by A2,FUNCT_1:8;
  hence p in f \/ g by XBOOLE_0:def 2; end;

theorem Th31:
   f tolerates g iff f \/ g = f +* g
 proof
  thus f tolerates g implies f \/ g = f +* g
   proof assume f tolerates g;
    then f c= f +* g & g c= f +* g by Th26,Th29;
    then f \/ g c= f +* g & f +* g c= f \/ g by Th30,XBOOLE_1:8;
    hence thesis by XBOOLE_0:def 10;
   end;
  thus thesis by PARTFUN1:130; end;

theorem Th32:
   dom f misses dom g implies f \/ g = f +* g
 proof assume dom f misses dom g; then f tolerates g by PARTFUN1:138;
  hence thesis by Th31; end;

theorem
     dom f misses dom g implies f c= f +* g
 proof assume dom f misses dom g;
  then f \/ g = f +* g by Th32;
  hence thesis by XBOOLE_1:7; end;

theorem
     dom f misses dom g implies (f +* g)|(dom f) = f
 proof assume dom f misses dom g;
then A1:   dom f \ dom g = dom f by XBOOLE_1:83;
A2:   dom((f +* g)|(dom f)) = dom(f +* g) /\ dom f by RELAT_1:90
                           .= (dom f \/ dom g) /\ dom f by Def1
                           .= dom f by XBOOLE_1:21;
     ((f +* g)|(dom f \ dom g)) c= f by Th25;
   hence (f +* g)|(dom f) = f by A1,A2,GRFUNC_1:9; end;

theorem Th35:
   f tolerates g iff f +* g = g +* f
 proof
  thus f tolerates g implies f +* g = g +* f
   proof assume
A1:  f tolerates g;
A2:  dom(f +* g) = dom g \/ dom f by Def1
                .= dom(g +* f) by Def1;
      for x st x in dom(f +* g) holds (f +* g).x = (g +* f).x
     proof let x such that
A3:    x in dom(f +* g);
        now
A4:     dom(f +* g) = dom f \/ dom g by Def1;
       per cases by A3,A4,XBOOLE_0:def 2;
       suppose x in dom f & x in dom g;
        then x in dom f /\ dom g & (f +* g).x = g.x & (g +* f).x = f.x
          by Th14,XBOOLE_0:def 3;
        hence (f +* g).x = (g +* f).x by A1,PARTFUN1:def 6;
       suppose x in dom f & not x in dom g;
        then (f +* g).x = f.x & (g +* f).x = f.x by Th12,Th14;
        hence (f +* g).x = (g +* f).x;
       suppose not x in dom f & x in dom g;
        then (f +* g).x = g.x & (g +* f).x = g.x by Th12,Th14;
        hence (f +* g).x = (g +* f).x;
      end;
      hence thesis;
     end;
    hence f +* g = g +* f by A2,FUNCT_1:9;
   end;
   assume
A5:   f +* g = g +* f;
   let x;
   assume x in dom f /\ dom g;
   then x in dom f & x in dom g by XBOOLE_0:def 3;
   then (f +* g).x = g.x & (g +* f).x = f.x by Th14;
   hence f.x = g.x by A5; end;

theorem
     dom f misses dom g implies f +* g = g +* f
 proof assume dom f misses dom g; then f tolerates g by PARTFUN1:138;
  hence thesis by Th35; end;

theorem
     for f,g being PartFunc of X,Y st g is total holds f +* g = g
 proof let f,g be PartFunc of X,Y;
  assume dom g = X; then dom f c= dom g;
  hence thesis by Th20; end;

theorem Th38:
   for f,g being Function of X,Y st Y = {} implies X = {} holds f +* g = g
 proof let f,g be Function of X,Y;
  assume Y = {} implies X = {}; then dom f = X & dom g = X by FUNCT_2:def 1;
  hence thesis by Th20; end;

theorem
     for f,g being Function of X,X holds f +* g = g
 proof let f,g be Function of X,X;
    X = {} implies X = {}; hence thesis by Th38; end;

theorem
     for f,g being Function of X,D holds f +* g = g by Th38;

theorem
     for f,g being PartFunc of X,Y holds f +* g is PartFunc of X,Y
 proof let f,g be PartFunc of X,Y;
    dom f c= X & dom g c= X & dom (f +* g) = dom f \/ dom g &
    rng (f +* g) c= rng f \/ rng g & rng f \/ rng g c= Y
     by Def1,Th18;
  then dom(f +* g) c= X & rng(f +* g) c= Y by XBOOLE_1:1;
  hence thesis by RELSET_1:11;
 end;

:: The converse function whenever domain

definition let f;
 func ~f -> Function means :Def2:
  (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]);
 existence
  proof
   defpred P[set] means ex y st [$1,y] in dom f;
   consider D1 being set such that
A1:   x in D1 iff x in union union dom f & P[x] from Separation;
   defpred P[set] means ex y st [y,$1] in dom f;
   consider D2 being set such that
A2:   y in D2 iff y in union union dom f & P[y] from Separation;
   defpred P[set] means ex y,z st $1 = [z,y] & [y,z] in dom f;
   consider D being set such that
A3:   x in D iff x in [:D2,D1:] & P[x] from Separation;
   defpred P[set,set] means ex y,z st $1 = [z,y] & $2 = f.[y,z];
A4:   for x,y1,y2 st x in D & P[x,y1] & P[x,y2] holds y1 = y2
     proof let x,y1,y2 such that x in D;
       given y,z such that
A5:      x = [z,y] and
A6:      y1 = f.[y,z];
       given y',z' such that
A7:      x = [z',y'] and
A8:      y2 = f.[y',z'];
         z = z' & y = y' by A5,A7,ZFMISC_1:33;
       hence thesis by A6,A8;
     end;
A9:  for x st x in D ex y1 st P[x,y1]
    proof let x; assume x in D;
     then consider y,z such that
A10:    x = [z,y] and [y,z] in dom f by A3;
     take f.[y,z];
     thus thesis by A10;
    end;
   consider h being Function such that
A11:  dom h = D and
A12:  for x st x in D holds P[x,h.x] from FuncEx(A4,A9);
   take h;
   thus
A13:   for x holds x in dom h iff ex y,z st x = [z,y] & [y,z] in dom f
    proof let x;
     thus x in dom h implies ex y,z st x = [z,y] & [y,z] in dom f by A3,A11;
     given y,z such that
A14:    x = [z,y] and
A15:    [y,z] in dom f;
       z in union union dom f & y in union union dom f by A15,Lm1;
     then y in D1 & z in D2 by A1,A2,A15;
     then [z,y] in [:D2,D1:] by ZFMISC_1:106;
     hence thesis by A3,A11,A14,A15;
    end;
   let y,z;
   assume [y,z] in dom f;
   then [z,y] in D by A11,A13;
   then consider y',z' such that
A16:   [z,y] = [z',y'] and
A17:   h.[z,y] =f.[y',z'] by A12;
     z = z' & y = y' by A16,ZFMISC_1:33;
   hence h.[z,y] = f.[y,z] by A17;
  end;
 uniqueness
  proof let h1,h2 be Function such that
A18:  for x holds x in dom h1 iff ex y,z st x = [z,y] & [y,z] in dom f and
A19:  for y,z st [y,z] in dom f holds h1.[z,y] = f.[y,z] and
A20:  for x holds x in dom h2 iff ex y,z st x = [z,y] & [y,z] in dom f and
A21:  for y,z st [y,z] in dom f holds h2.[z,y] = f.[y,z];
     x in dom h1 iff x in dom h2
    proof x in dom h1 iff ex y,z st x = [z,y] & [y,z] in dom f by A18;
     hence thesis by A20;
    end;
then A22:  dom h1 = dom h2 by TARSKI:2;
     x in dom h1 implies h1.x = h2.x
    proof assume x in dom h1;
     then consider x1,x2 such that
A23:   x = [x2,x1] and
A24:   [x1,x2] in dom f by A18;
     thus h1.x = f.[x1,x2] by A19,A23,A24 .= h2.x by A21,A23,A24;
    end;
   hence thesis by A22,FUNCT_1:9;
  end;
end;

theorem Th42:
   rng ~f c= rng f
 proof let y; assume y in rng ~f;
  then consider x such that
A1:  x in dom ~f and
A2:  y = (~f).x by FUNCT_1:def 5;
  consider x1,x2 such that
A3:  x = [x2,x1] and
A4:  [x1,x2] in dom f by A1,Def2;
    y = f.[x1,x2] by A2,A3,A4,Def2;
  hence thesis by A4,FUNCT_1:def 5; end;

theorem Th43:
   [x,y] in dom f iff [y,x] in dom ~f
 proof thus [x,y] in dom f implies [y,x] in dom ~f by Def2;
  assume [y,x] in dom ~f;
  then consider x1,y1 such that
A1:  [y,x] = [y1,x1] and
A2:  [x1,y1] in dom f by Def2;
    x1 = x & y1 = y by A1,ZFMISC_1:33;
  hence thesis by A2; end;

theorem
     [y,x] in dom ~f implies (~f).[y,x] = f.[x,y]
 proof assume [y,x] in dom ~f; then [x,y] in dom f by Th43;
  hence thesis by Def2; end;

theorem
     ex X,Y st dom ~f c= [:X,Y:]
 proof
    now let z; assume z in dom ~f;
   then ex x,y st z = [y,x] & [x,y] in dom f by Def2;
   hence ex x,y st z = [x,y];
  end;
  hence thesis by Th1; end;

theorem Th46:
   dom f c= [:X,Y:] implies dom ~f c= [:Y,X:]
 proof assume
A1: dom f c= [:X,Y:];
  let z; assume z in dom ~f;
  then consider x,y such that
A2:  z = [y,x] and
A3:  [x,y] in dom f by Def2;
  thus thesis by A1,A2,A3,ZFMISC_1:107; end;

theorem Th47:
   dom f = [:X,Y:] implies dom ~f = [:Y,X:]
 proof assume
A1:  dom f = [:X,Y:];
  hence dom ~f c= [:Y,X:] by Th46;
  let z; assume z in [:Y,X:];
  then consider y,x such that
A2:  y in Y & x in X and
A3:  z = [y,x] by ZFMISC_1:def 2;
    [x,y] in dom f by A1,A2,ZFMISC_1:def 2;
  hence thesis by A3,Def2; end;

theorem Th48:
   dom f c= [:X,Y:] implies rng ~f = rng f
 proof assume
A1:  dom f c= [:X,Y:];
  thus rng ~f c= rng f by Th42;
  let y; assume y in rng f;
  then consider x such that
A2:  x in dom f and
A3:  y = f.x by FUNCT_1:def 5;
  consider x1,y1 such that x1 in X & y1 in Y and
A4:  x =[x1,y1] by A1,A2,ZFMISC_1:103;
    [y1,x1] in dom ~f & y = (~f).[y1,x1] by A2,A3,A4,Def2;
  hence y in rng ~f by FUNCT_1:def 5; end;

theorem
     for f being PartFunc of [:X,Y:],Z holds ~f is PartFunc of [:Y,X:],Z
 proof let f be PartFunc of [:X,Y:],Z;
    dom f c= [:X,Y:] & rng f c= Z;
   then dom ~f c= [:Y,X:] & rng ~f c= Z by Th46,Th48;
  hence thesis by RELSET_1:11;
  end;

theorem Th50:
   for f being Function of [:X,Y:],Z st Z<>{} holds ~f is Function of [:Y,X:],Z
 proof let f be Function of [:X,Y:],Z;
  assume
A1:  Z <> {};
   then dom f = [:X,Y:] & rng f c= Z by FUNCT_2:def 1;
   then [:Y,X:] = dom ~f & rng ~f c= Z by Th47,Th48;
  then reconsider R = ~f as Relation of [:Y,X:],Z by RELSET_1:11;
    R is quasi_total
  proof
  per cases;
  case Z = {} implies [:Y,X:] = {};
     dom f = [:X,Y:] & rng f c= Z by A1,FUNCT_2:def 1;
   hence [:Y,X:] = dom R by Th47;
  case Z = {} & [:Y,X:] <> {};
   hence thesis by A1;
  end;
  hence thesis;
 end;

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

theorem Th52:
    ~~f c= f
 proof
A1: now let x;
     assume x in dom ~~f;
     then consider y2,z2 such that
A2:   x = [z2,y2] and
A3:   [y2,z2] in dom ~f by Def2;
    take y2,z2;
    thus x = [z2,y2] & [y2,z2] in dom ~ f & [z2,y2] in dom f by A2,A3,Th43;
   end;
A4:  dom ~~f c= dom f
   proof let x;
    assume x in dom ~~f;
    then ex y2,z2 st x = [z2,y2] & [y2,z2] in dom ~ f & [z2,y2] in dom f by A1
;
    hence x in dom f;
   end;
    x in dom ~~f implies (~~f).x = f.x
   proof assume x in dom ~~f;
     then consider y2,z2 such that
A5:   x = [z2,y2] and
A6:   [y2,z2] in dom ~f and
A7:   [z2,y2] in dom f by A1;
    thus (~~f).x = (~f).[y2,z2] by A5,A6,Def2 .= f.x by A5,A7,Def2;
   end;
  hence thesis by A4,GRFUNC_1:8; end;

theorem Th53:
   dom f c= [:X,Y:] implies ~~f = f
 proof assume
A1:  dom f c= [:X,Y:];
A2:   ~~f c= f by Th52;
    dom ~~ f = dom f
   proof thus dom ~~f c= dom f by A2,RELAT_1:25;
    let z; assume
A3:   z in dom f;
    then consider x,y such that x in X & y in Y and
A4:   z = [x,y] by A1,ZFMISC_1:103;
      [y,x] in dom ~f by A3,A4,Th43;
    hence thesis by A4,Th43;
   end;
  hence thesis by A2,GRFUNC_1:9; end;

theorem
     for f being PartFunc of [:X,Y:],Z holds ~~f = f
 proof let f be PartFunc of [:X,Y:],Z;
    dom f c= [:X,Y:]; hence thesis by Th53; end;

theorem Th55:
   for f being Function of [:X,Y:],Z st Z <> {} holds ~~f = f
 proof let f be Function of [:X,Y:],Z;
  assume Z <> {}; then dom f = [:X,Y:] by FUNCT_2:def 1;
  hence thesis by Th53; end;

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

:: Product of 2'ary functions

definition let f,g;
  func |:f,g:| -> Function means
:Def3:
  (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']]);
 existence
  proof
   defpred P[set] means ex y st [$1,y] in dom f;
   consider D1 being set such that
A1:   x in D1 iff x in union union dom f & P[x] from Separation;
   defpred P[set] means ex x st [x,$1] in dom f;
   consider D2 being set such that
A2:   y in D2 iff y in union union dom f & P[y] from Separation;
   defpred P[set] means ex y st [$1,y] in dom g;
   consider D1' being set such that
A3:   x in D1' iff x in union union dom g & P[x] from Separation;
   defpred P[set] means ex x st [x,$1] in dom g;
   consider D2' being set such that
A4:   y in D2' iff y in union union dom g & P[y] from Separation;
   defpred P[set] means
   ex x,y,x',y' st $1 = [[x,x'],[y,y']] & [x,y] in dom f & [x',y'] in dom g;
   consider D being set such that
A5:   z in D iff z in [:[:D1,D1':],[:D2,D2':]:] & P[z] from Separation;
     defpred P[set,set] means
      ex x,y,x',y' st $1 = [[x,x'],[y,y']] & $2 = [f.[x,y],g.[x',y']];
A6:  for z,z1,z2 st z in D & P[z,z1] & P[z,z2] holds z1 = z2
    proof let z,z1,z2 such that z in D;
      given x,y,x',y' such that
A7:      z = [[x,x'],[y,y']] and
A8:      z1 = [f.[x,y],g.[x',y']];
      given x1,y1,x1',y1' such that
A9:     z = [[x1,x1'],[y1,y1']] and
A10:     z2 = [f.[x1,y1],g.[x1',y1']];
        x = x1 & y = y1 & x' = x1' & y' = y1' by A7,A9,Lm2;
      hence thesis by A8,A10;
    end;
A11:  for z st z in D holds ex z1 st P[z,z1]
    proof let z;
     assume z in D;
     then consider x,y,x',y' such that
A12:    z = [[x,x'],[y,y']] and [x,y] in dom f & [x',y'] in dom g by A5;
      take [f.[x,y],g.[x',y']];
      thus thesis by A12;
    end;
   consider h being Function such that
A13:   dom h = D and
A14:   for z st z in D holds P[z,h.z] from FuncEx(A6,A11);
   take h;
   thus
A15:  for z holds z in dom h iff
       ex x,y,x',y' st z = [[x,x'],[y,y']] & [x,y] in dom f & [x',y'] in dom g
    proof let z;
     thus z in dom h implies
        ex x,y,x',y' st z = [[x,x'],[y,y']] & [x,y] in dom f & [x',y'] in dom g
       by A5,A13;
     given x,y,x',y' such that
A16:    z = [[x,x'],[y,y']] and
A17:    [x,y] in dom f and
A18:    [x',y'] in dom g;
       x in union union dom f & y in union union dom f &
     x' in union union dom g & y' in union union dom g by A17,A18,Lm1;
     then x in D1 & y in D2 & x' in D1' & y' in D2' by A1,A2,A3,A4,A17,A18;
     then [x,x'] in [:D1,D1':] & [y,y'] in [:D2,D2':] by ZFMISC_1:106;
     then z in [:[:D1,D1':],[:D2,D2':]:] by A16,ZFMISC_1:106;
     hence z in dom h by A5,A13,A16,A17,A18;
    end;
   let x,y,x',y' such that
A19:   [x,y] in dom f and
A20:   [x',y'] in dom g;
     [[x,x'],[y,y']] in D by A13,A15,A19,A20;
   then consider x1,y1,x1',y1' such that
A21:   [[x,x'],[y,y']] = [[x1,x1'],[y1,y1']] and
A22:   h.[[x,x'],[y,y']] = [f.[x1,y1],g.[x1',y1']] by A14;
     x = x1 & y = y1 & x'= x1' & y' = y1' by A21,Lm2;
   hence h.[[x,x'],[y,y']] = [f.[x,y],g.[x',y']] by A22;
  end;
 uniqueness
  proof let h1,h2 be Function such that
A23:  for z holds z in dom h1 iff
      ex x,y,x',y' st z = [[x,x'],[y,y']] & [x,y] in dom f & [x',y'] in
 dom g and
A24:  for x,y,x',y' st [x,y] in dom f & [x',y'] in dom g
       holds h1.[[x,x'],[y,y']] = [f.[x,y],g.[x',y']] and
A25:  for z holds z in dom h2 iff
      ex x,y,x',y' st z = [[x,x'],[y,y']] & [x,y] in dom f & [x',y'] in
 dom g and
A26:  for x,y,x',y' st [x,y] in dom f & [x',y'] in dom g
       holds h2.[[x,x'],[y,y']] = [f.[x,y],g.[x',y']];
       z in dom h1 iff z in dom h2
      proof
          z in dom h1 iff
          ex x,y,x',y' st z = [[x,x'],[y,y']] & [x,y] in dom f & [x',y'] in
 dom g
        by A23;
        hence thesis by A25;
      end;
then A27:  dom h1 = dom h2 by TARSKI:2;
      z in dom h1 implies h1.z = h2.z
     proof assume z in dom h1;
      then consider x,y,x',y' such that
A28:     z = [[x,x'],[y,y']] & [x,y] in dom f & [x',y'] in dom g by A23;
      thus h1.z = [f.[x,y],g.[x',y']] by A24,A28 .= h2.z by A26,A28;
     end;
    hence thesis by A27,FUNCT_1:9;
  end;
end;

theorem Th57:
   [[x,x'],[y,y']] in dom |:f,g:| iff [x,y] in dom f & [x',y'] in dom g
 proof
   thus [[x,x'],[y,y']] in dom |:f,g:| implies [x,y] in dom f & [x',y'] in
 dom g
    proof assume [[x,x'],[y,y']] in dom |:f,g:|;
     then consider x1,y1,x1',y1' such that
A1:   [[x,x'],[y,y']] = [[x1,x1'],[y1,y1']] and
A2:   [x1,y1] in dom f & [x1',y1'] in dom g by Def3;
       x = x1 & y = y1 & x'= x1' & y' = y1' by A1,Lm2;
     hence thesis by A2;
    end;
   thus thesis by Def3; end;

theorem
     [[x,x'],[y,y']] in dom |:f,g:|
     implies |:f,g:|.[[x,x'],[y,y']] = [f.[x,y],g.[x',y']]
 proof assume [[x,x'],[y,y']] in dom |:f,g:|;
   then [x,y] in dom f & [x',y'] in dom g by Th57;
   hence thesis by Def3; end;

theorem Th59:
   rng |:f,g:| c= [:rng f,rng g:]
 proof let z;
  assume z in rng |:f,g:|;
  then consider p such that
A1: p in dom |:f,g:| and
A2: z = |:f,g:|.p by FUNCT_1:def 5;
  consider x,y,x',y' such that
A3:  p = [[x,x'],[y,y']] and
A4:  [x,y] in dom f & [x',y'] in dom g by A1,Def3;
    f.[x,y] in rng f & g.[x',y'] in rng g by A4,FUNCT_1:def 5;
  then [f.[x,y],g.[x',y']] in [:rng f,rng g:] by ZFMISC_1:106;
  hence z in [:rng f,rng g:] by A2,A3,A4,Def3; end;

theorem Th60:
   dom f c= [:X,Y:] & dom g c= [:X',Y':]
     implies dom|:f,g:| c= [:[:X,X':],[:Y,Y':]:]
 proof assume
A1:   dom f c= [:X,Y:] & dom g c= [:X',Y':];
  let xy be set;
  assume xy in dom|:f,g:|;
  then consider x,y,x',y' such that
A2:  xy = [[x,x'],[y,y']] and
A3:  [x,y] in dom f & [x',y'] in dom g by Def3;
    x in X & y in Y & x' in X' & y' in Y' by A1,A3,ZFMISC_1:106;
  then [x,x'] in [:X,X':] & [y,y'] in [:Y,Y':] by ZFMISC_1:106;
  hence xy in [:[:X,X':],[:Y,Y':]:] by A2,ZFMISC_1:106; end;

theorem Th61:
   dom f = [:X,Y:] & dom g = [:X',Y':]
     implies dom|:f,g:| = [:[:X,X':],[:Y,Y':]:]
 proof assume
A1: dom f = [:X,Y:] & dom g = [:X',Y':];
   hence dom|:f,g:| c= [:[:X,X':],[:Y,Y':]:] by Th60;
   let z; assume z in [:[:X,X':],[:Y,Y':]:];
   then consider xx,yy being set such that
A2:  xx in [:X,X':] and
A3:  yy in [:Y,Y':] and
A4:  z = [xx,yy] by ZFMISC_1:def 2;
   consider x,x' such that
A5:  x in X & x' in X' and
A6:  xx = [x,x'] by A2,ZFMISC_1:def 2;
   consider y,y' such that
A7:  y in Y & y' in Y' and
A8:  yy = [y,y'] by A3,ZFMISC_1:def 2;
     [x,y] in dom f & [x',y'] in dom g by A1,A5,A7,ZFMISC_1:106;
   hence thesis by A4,A6,A8,Def3; end;

theorem
     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':]
 proof let f be PartFunc of [:X,Y:],Z; let g be PartFunc of [:X',Y':],Z';
    dom f c= [:X,Y:] & dom g c= [:X',Y':];
   then A1:  dom|:f,g:| c= [:[:X,X':],[:Y,Y':]:] by Th60;
    rng |:f,g:| c= [:rng f,rng g:] & [:rng f,rng g:] c= [:Z,Z':]
   by Th59,ZFMISC_1:119;
   then rng|:f,g:| c= [:Z,Z':] by XBOOLE_1:1;
  hence thesis by A1,RELSET_1:11;
  end;

theorem Th63:
   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':]
 proof let f be Function of [:X,Y:],Z; let g be Function of [:X',Y':],Z';
  assume
A1:  Z <> {} & Z' <> {};
   then dom f = [:X,Y:] & dom g = [:X',Y':] by FUNCT_2:def 1;
   then A2:  [:[:X,X':],[:Y,Y':]:] = dom|:f,g:| by Th61;
     rng |:f,g:| c= [:rng f,rng g:] & [:rng f,rng g:] c= [:Z,Z':]
    by Th59,ZFMISC_1:119;
   then rng|:f,g:| c= [:Z,Z':] by XBOOLE_1:1;
  then reconsider R = |:f,g:| as Relation of [:[:X,X':],[:Y,Y':]:],[:Z,Z':]
       by A2,RELSET_1:11;
    R is quasi_total
  proof
  per cases;
  case [:Z,Z':] = {} implies [:[:X,X':],[:Y,Y':]:] = {};
     dom f = [:X,Y:] & dom g = [:X',Y':] by A1,FUNCT_2:def 1;
   hence [:[:X,X':],[:Y,Y':]:] = dom R by Th61;
   thus thesis;
  case [:Z,Z':] = {} & [:[:X,X':],[:Y,Y':]:] <> {};
   hence thesis by A1,ZFMISC_1:113;
  end;
  hence thesis;
 end;

theorem
     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':] by Th63;

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

definition let x,y,a,b be set;
  cluster (x,y) --> (a,b) -> Function-like Relation-like;
 coherence
 proof
    ({x} --> a) +* ({y} --> b) = (x,y) --> (a,b) by Def4;
  hence thesis;
 end;
end;

theorem Th65:
  dom((x1,x2) --> (y1,y2)) = {x1,x2} & rng((x1,x2) --> (y1,y2)) c= {y1,y2}
 proof set f = {x1} --> y1, g = {x2} -->y2, h = (x1,x2) --> (y1,y2);
A1:  h = f +* g by Def4;
    dom f = {x1} & dom g = {x2} by FUNCOP_1:19;
  then dom f \/ dom g = {x1,x2} by ENUMSET1:41;
  hence dom h = {x1,x2} by A1,Def1;
    rng f c= {y1} & rng g c= {y2} by FUNCOP_1:19;
  then rng f \/ rng g c= {y1} \/ {y2} by XBOOLE_1:13;
  then rng f \/ rng g c= {y1,y2} & rng h c= rng f \/ rng g
   by A1,Th18,ENUMSET1:41;
  hence rng h c= {y1,y2} by XBOOLE_1:1;
 end;

theorem Th66:
  x1 <> x2 implies
    ((x1,x2) --> (y1,y2)).x1 = y1 & ((x1,x2) --> (y1,y2)).x2 = y2
proof set f = {x1} --> y1, g = {x2} -->y2, h = (x1,x2) --> (y1,y2);
 assume
A1:  x1 <> x2;
A2:  h = f +* g by Def4;
A3:  x1 in {x1} & x2 in {x2} by TARSKI:def 1;
A4:  {x1} = dom f & {x2} = dom g by FUNCOP_1:19;
 then not x1 in dom g by A1,TARSKI:def 1;
 then h.x1 = f.x1 by A2,Th12;
 hence h.x1 = y1 by A3,FUNCOP_1:13;
   h.x2 = g.x2 by A2,A3,A4,Th14;
 hence h.x2 = y2 by A3,FUNCOP_1:13;
end;

theorem
    x1 <> x2 implies rng((x1,x2) --> (y1,y2)) = {y1,y2}
 proof set h = (x1,x2) --> (y1,y2);
  assume
A1:  x1 <> x2;
  thus rng h c= {y1,y2} by Th65;
  let y;
  assume y in {y1,y2};
  then (y = y1 or y = y2) & dom h = {x1,x2} by Th65,TARSKI:def 2;
  then (h.x1 = y or h.x2 = y) & x1 in dom h & x2 in dom h
    by A1,Th66,TARSKI:def 2;
  hence y in rng h by FUNCT_1:def 5;
 end;

theorem
    (x1,x2) --> (y,y) = {x1,x2} --> y
 proof set F = (x1,x2)-->(y,y), f = {x1}-->y, g = {x2}-->y, F' = {x1,x2}-->y;
A1:  F = f +* g by Def4;
    now thus
A2:  dom F = {x1,x2} & dom F' = {x1,x2} by Th65,FUNCOP_1:19;
   let x such that
A3:  x in {x1,x2};
     now per cases by A1,A2,A3,Th13;
    suppose x in dom f & not x in dom g;
     then F.x = f.x & x in {x1} by A1,Th12,FUNCOP_1:19;
     hence F.x = y & F'.x = y by A3,FUNCOP_1:13;
    suppose x in dom g;
     then F.x = g.x & x in {x2} by A1,Th14,FUNCOP_1:19;
     hence F.x = y & F'.x = y by A3,FUNCOP_1:13;
   end;
   hence F.x = F'.x;
  end;
  hence thesis by FUNCT_1:9;
 end;

definition let A,x1,x2; let y1,y2 be Element of A;
  redefine func (x1,x2) --> (y1,y2) -> Function of {x1,x2},A;
  coherence
 proof set f = {x1} --> y1, g = {x2} -->y2, h = (x1,x2) --> (y1,y2);
    now
   thus dom h = {x1,x2} by Th65;
     rng f c= {y1} & rng g c= {y2} by FUNCOP_1:19;
   then rng f \/ rng g c= {y1} \/ {y2} & {y1} \/ {y2} = {y1,y2} &
    {y1,y2} c= A &
     h = f +* g by Def4,ENUMSET1:41,XBOOLE_1:13,ZFMISC_1:38;
   then rng f \/ rng g c= A & rng h c= rng f \/ rng g by Th18,XBOOLE_1:1;
   hence rng h c= A by XBOOLE_1:1;
  end;
  hence h is Function of {x1,x2},A by FUNCT_2:def 1,RELSET_1:11;
 end;
end;

theorem
   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)
 proof let a,b,c,d be set;
  let h be Function such that
A1:dom h = {a,b} & h.a = c & h.b = d;
   set f = {a} --> c, g = {b} -->d;
A2: a in {a} & b in {b} by TARSKI:def 1;
A3: dom f = {a} & dom g = {b} by FUNCOP_1:19;
then A4: dom h = dom f \/ dom g by A1,ENUMSET1:41;
     now let x such that
A5: x in dom f \/ dom g;
    thus x in dom g implies h.x = g.x
     proof assume x in dom g;
       then x = b by A3,TARSKI:def 1;
      hence h.x = g.x by A1,A2,FUNCOP_1:13;
     end;
    assume not x in dom g;
     then x in dom f by A5,XBOOLE_0:def 2;
     then x = a by A3,TARSKI:def 1;
    hence h.x = f.x by A1,A2,FUNCOP_1:13;
   end;
  hence h = f +* g by A4,Def1
     .= (a,b) --> (c,d) by Def4;
 end;

theorem Th70:
 for x,y being set holds {x} --> y = {[x,y]}
  proof let x,y be set;
   thus {x} --> y = [:{x},{y}:] by FUNCOP_1:def 2
     .= {[x,y]} by ZFMISC_1:35;
  end;

theorem
   for a,b,c,d being set st a <> c
  holds (a,c) --> (b,d) = { [a,b], [c,d] }
 proof let a,b,c,d be set such that
A1: a <> c;
    set f = {a} --> b, g = {c} --> d;
A2: {a} --> b = {[a,b]} & {c} --> d = {[c,d]} by Th70;
A3: {a} misses {c} by A1,ZFMISC_1:17;
A4: dom f = {a} & dom g = {c} by FUNCOP_1:19;
  thus (a,c) --> (b,d) = f +* g by Def4
    .= {[a,b]} \/ {[c,d]} by A2,A3,A4,Th32
    .= { [a,b], [c,d] } by ENUMSET1:41;
 end;

theorem
   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'
proof let a,b,x,y,x',y' be set such that
A1: a <> b and
A2: (a,b) --> (x,y) = (a,b) --> (x',y');
 thus x = ((a,b) --> (x,y)).a by A1,Th66
         .= x' by A1,A2,Th66;
 thus y = ((a,b) --> (x,y)).b by A1,Th66
         .= y' by A1,A2,Th66;
end;


Back to top