:: Function Domains and Fr{\ae}nkel Operator
::  by Andrzej Trybulec
::
:: Received February 7, 1990
:: Copyright (c) 1990-2012 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 XBOOLE_0, SUBSET_1, TARSKI, FUNCT_1, RELAT_1, FUNCT_2, ZFMISC_1,
      PARTFUN1, FINSET_1, MCART_1, FINSUB_1, SETWISEO;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XTUPLE_0, MCART_1, RELAT_1,
      FINSET_1, FINSUB_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1,
      DOMAIN_1, SETWISEO;
 constructors PARTFUN1, BINOP_1, DOMAIN_1, FINSET_1, SETWISEO, RELSET_1,
      XTUPLE_0;
 registrations SUBSET_1, RELAT_1, FINSET_1, FINSUB_1, RELSET_1, XTUPLE_0;
 requirements BOOLE, SUBSET;
 definitions TARSKI, XBOOLE_0, FUNCT_1, BINOP_1, XTUPLE_0;
 theorems FINSET_1, ZFMISC_1, MCART_1, FUNCT_1, FUNCT_2, FINSUB_1, RELAT_1,
      RELSET_1, XBOOLE_0, XBOOLE_1, TARSKI, SUBSET_1;
 schemes FUNCT_1, FUNCT_2, SETWISEO, DOMAIN_1, PARTFUN1;

begin

reserve B for non empty set,
  A,X,x for set;

scheme
  Fraenkel59{ A() -> set, F(set) -> set, P,Q[set] } :
  { F(v) where v is Element of A() : P[v] } c=
   { F(u) where u is Element of A() : Q[u] }
provided
A1: for v being Element of A() holds P[v] implies Q[v]
proof
  let x be set;
  assume x in { F(v9) where v9 is Element of A() : P[v9] };
  then consider v being Element of A() such that
A2: x = F(v) and
A3: P[v];
  Q[v] by A1,A3;
  hence thesis by A2;
end;

scheme
  Fraenkel599 { A,B() -> set, F(set,set) -> set, P,Q[set,set] } :
  { F(u1,v1) where u1 is Element of A(), v1 is Element of B() : P[u1,v1] } c=
  { F(u2,v2) where u2 is Element of A(), v2 is Element of B() : Q[u2,v2] }
provided
A1: for u being (Element of A()), v being Element of B() holds P[u,v]
implies Q[u,v]
proof
  let x be set;
  assume x in {F(u9,v9) where u9 is (Element of A()), v9 is Element of B() :
  P[u9,v9]};
  then consider u being (Element of A()), v being Element of B() such that
A2: x = F(u,v) and
A3: P[u,v];
  Q[u,v] by A1,A3;
  hence thesis by A2;
end;

scheme
  Fraenkel69{ B() -> set, F(set) -> set, P, Q[set] } :
  { F(v1) where v1 is Element of B() : P[v1] } =
  { F(v2) where v2 is Element of B() : Q[v2] }
provided
A1: for v being Element of B() holds P[v] iff Q[v]
proof
  set A = { F(v1) where v1 is Element of B() : P[v1] }, B = { F(v2) where v2
  is Element of B() : Q[v2] };
A2: for v being Element of B() holds P[v] implies Q[v] by A1;
  thus A c= B from Fraenkel59(A2);
A3: for v being Element of B() holds Q[v] implies P[v] by A1;
  thus B c= A from Fraenkel59(A3);
end;

scheme
  Fraenkel699 { A,B() -> set, F(set,set) -> set, P,Q[set,set] } :
  { F(u1,v1) where u1 is Element of A(), v1 is Element of B() : P[u1,v1] } =
  { F(u2,v2) where u2 is Element of A(), v2 is Element of B() : Q[u2,v2] }
provided
A1: for u being Element of A(), v being Element of B() holds P[u,v]
iff Q[u,v]
proof
  set B = { F(u2,v2) where u2 is (Element of A()), v2 is Element of B() : Q[u2
  ,v2] };
  set A = { F(u1,v1) where u1 is (Element of A()), v1 is Element of B() : P[u1
  ,v1] };
A2: for u being (Element of A()), v being Element of B() holds P[u,v]
  implies Q[u,v] by A1;
  thus A c= B from Fraenkel599(A2);
A3: for u being (Element of A()), v being Element of B() holds Q[u,v]
  implies P[u,v] by A1;
  thus B c= A from Fraenkel599(A3);
end;

scheme
  FraenkelF9{ B() -> set, F,G(set) -> set, P[set] } :
  { F(v1) where v1 is Element of B() : P[v1] } =
  { G(v2) where v2 is Element of B() : P[v2] }
provided
A1: for v being Element of B() holds F(v) = G(v)
proof
  set X = { F(v1) where v1 is Element of B() : P[v1] }, Y = { G(v2) where v2
  is Element of B() : P[v2] };
A2: Y c= X
  proof
    let x be set;
    assume x in Y;
    then consider v1 being Element of B() such that
A3: x = G(v1) and
A4: P[v1];
    x = F(v1) by A1,A3;
    hence thesis by A4;
  end;
  X c= Y
  proof
    let x be set;
    assume x in X;
    then consider v1 being Element of B() such that
A5: x = F(v1) and
A6: P[v1];
    x = G(v1) by A1,A5;
    hence thesis by A6;
  end;
  hence thesis by A2,XBOOLE_0:def 10;
end;

scheme
  FraenkelF9R{ B() -> set, F,G(set) -> set, P[set] } :
  { F(v1) where v1 is Element of B() : P[v1] } =
  { G(v2) where v2 is Element of B() : P[v2] }
provided
A1: for v being Element of B() st P[v] holds F(v) = G(v)
proof
  set X = { F(v1) where v1 is Element of B() : P[v1] }, Y = { G(v2) where v2
  is Element of B() : P[v2] };
A2: Y c= X
  proof
    let x be set;
    assume x in Y;
    then consider v1 being Element of B() such that
A3: x = G(v1) and
A4: P[v1];
    x = F(v1) by A1,A3,A4;
    hence thesis by A4;
  end;
  X c= Y
  proof
    let x be set;
    assume x in X;
    then consider v1 being Element of B() such that
A5: x = F(v1) and
A6: P[v1];
    x = G(v1) by A1,A5,A6;
    hence thesis by A6;
  end;
  hence thesis by A2,XBOOLE_0:def 10;
end;

scheme
  FraenkelF99 { A,B() -> set, F(set,set) -> set, G(set,set) -> set,
                P[set,set] } :
  { F(u1,v1) where u1 is Element of A(), v1 is Element of B() : P[u1,v1] } =
  { G(u2,v2) where u2 is Element of A(), v2 is Element of B() : P[u2,v2] }
provided
A1: for u being Element of A(), v being Element of B() holds F(u,v) = G(u,v)
proof
  set Y = { G(u2,v2) where u2 is (Element of A()), v2 is Element of B() : P[u2
  ,v2] };
  set X = { F(u1,v1) where u1 is (Element of A()), v1 is Element of B() : P[u1
  ,v1] };
A2: Y c= X
  proof
    let x be set;
    assume x in Y;
    then consider u1 being (Element of A()), v1 being Element of B() such that
A3: x = G(u1,v1) and
A4: P[u1,v1];
    x = F(u1,v1) by A1,A3;
    hence thesis by A4;
  end;
  X c= Y
  proof
    let x be set;
    assume x in X;
    then consider u1 being (Element of A()), v1 being Element of B() such that
A5: x = F(u1,v1) and
A6: P[u1,v1];
    x = G(u1,v1) by A1,A5;
    hence thesis by A6;
  end;
  hence thesis by A2,XBOOLE_0:def 10;
end;

scheme
  FraenkelF699 { A,B() -> set, F(set,set) -> set, P,Q[set,set] } :
  { F(u1,v1) where u1 is Element of A(), v1 is Element of B() : P[u1,v1] } =
  { F(v2,u2) where u2 is Element of A(), v2 is Element of B() : Q[u2,v2] }
provided
A1: for u being Element of A(), v being Element of B() holds P[u,v]
iff Q[u,v] and
A2: for u being Element of A(), v being Element of B() holds F(u,v) = F(v,u)
proof
A3: for u being Element of A(), v being Element of B() holds Q[u,v]
  implies P[u,v] by A1;
A4: { F(u1,v1) where u1 is (Element of A()), v1 is Element of B() : Q[u1,v1]
} c= { F(u2,v2) where u2 is (Element of A()), v2 is Element of B() : P[u2,v2] }
  from Fraenkel599(A3);
  deffunc H(set,set) = F($2,$1);
A5: for u being (Element of A()), v being Element of B() holds P[u,v]
  implies Q[u,v] by A1;
A6: { F(u1,v1) where u1 is (Element of A()), v1 is Element of B() : P[u1,v1]
} c= { F(u2,v2) where u2 is (Element of A()), v2 is Element of B() : Q[u2,v2] }
  from Fraenkel599(A5);
A7: for u being Element of A(), v being Element of B() holds F(u,v) = H(u,v)
  by A2;
  { F(u1,v1) where u1 is Element of A(), v1 is Element of B() : Q[u1,v1] }
= { H(u2,v2) where u2 is Element of A(), v2 is Element of B() : Q[u2,v2] } from
  FraenkelF99(A7);
  hence thesis by A6,A4,XBOOLE_0:def 10;
end;

theorem Th1:
  for A,B being  set, F,G being Function of A,B for X
  being set st F|X = G|X for x being Element of A st x in X holds F.x = G.x
proof
  let A,B be set, F,G be Function of A,B;
  let X be set such that
A1: F|X = G|X;
  let x be Element of A;
  assume
A2: x in X;
  hence F.x = (G|X).x by A1,FUNCT_1:49
    .= G.x by A2,FUNCT_1:49;
end;

theorem Th2:
  for A,B being set holds Funcs(A,B) c= bool [:A,B:]
proof
  let A,B be set, x be set;
  assume x in Funcs(A,B);
  then consider f being Function such that
A1: x = f and
A2: dom f = A and
A3: rng f c= B by FUNCT_2:def 2;
A4: f c= [: dom f, rng f:] by RELAT_1:7;
  [:dom f, rng f:] c= [:A,B:] by A2,A3,ZFMISC_1:95;
  then f c= [:A,B:] by A4,XBOOLE_1:1;
  hence thesis by A1;
end;

theorem Th3:
  for X,Y being set st Funcs(X,Y) <> {} & X c= A & Y c= B for f
  being Element of Funcs(X,Y) holds f is PartFunc of A,B
proof
  let X,Y be set such that
A1: Funcs(X,Y) <> {} and
A2: X c= A and
A3: Y c= B;
  let f be Element of Funcs(X,Y);
  consider g being Function such that
A4: f = g and
A5: dom g = X and
A6: rng g c= Y by A1,FUNCT_2:def 2;
  rng g c= B by A3,A6,XBOOLE_1:1;
  hence thesis by A2,A4,A5,RELSET_1:4;
end;

scheme
  RelevantArgs
  { A,B,X() -> set, f,g() -> Function of A(),B(), P[set], Q[set] } :
  { f().u9 where u9 is Element of A() : P[u9] & u9 in X() } =
  { g().v9 where v9 is Element of A() : Q[v9] & v9 in X() }
provided
A1: f()|X() = g()|X() and
A2: for u being Element of A() st u in X() holds P[u] iff Q[u]
proof
  deffunc F(set) = f().$1;
  deffunc G(set) = g().$1;
  defpred PP[set] means P[$1] & $1 in X();
  defpred QQ[set] means Q[$1] & $1 in X();
  set C = { G(v9) where v9 is Element of A() : PP[v9] };
A3: for v being Element of A() holds PP[v] iff QQ[v] by A2;
A4: C = { G(v9) where v9 is Element of A() : QQ[v9] } from Fraenkel69(A3);
A5: for v being Element of A() st PP[v] holds F(v) = G(v) by A1,Th1;
  { F(u9) where u9 is Element of A() : PP[u9] } = C from FraenkelF9R(A5);
  hence thesis by A4;
end;

scheme
  FrSet0{ A() -> non empty set, P[set] }:
  { x where x is Element of A(): P[x] } c= A()
proof
  { x where x is Element of A(): P[x] } is Subset of A() from DOMAIN_1:sch 7;
  hence thesis;
end;

scheme
  Gen199{A,B() -> set, F(set,set) -> set, P[set,set], Q[set] } :
  for s being Element of A(), t being Element of B() st P[s,t] holds Q[F(s,t)]
provided
A1: for st1 being set st st1 in { F(s1,t1) where s1 is (Element of A()),
t1 is Element of B(): P[s1,t1] } holds Q[st1]
proof
  let s be (Element of A()), t be Element of B();
  assume P[s,t];
  then
  F(s,t) in { F(s1,t1) where s1 is (Element of A()), t1 is Element of B():
  P[s1,t1] };
  hence thesis by A1;
end;

scheme
  Gen199A{A,B() -> set, F(set,set) -> set, P[set,set], Q[set] } :
  for st1 being set st st1 in { F(s1,t1) where s1 is Element of A(),
  t1 is Element of B(): P[s1,t1] } holds Q[st1]
provided
A1: for s being Element of A(), t being Element of B() st P[s,t] holds
    Q[F(s,t)]
proof
  let st1 be set;
  assume st1 in { F(s1,t1) where s1 is (Element of A()), t1 is Element of B()
  : P[s1,t1] };
  then
  ex s1 being (Element of A()), t1 being Element of B() st st1 = F(s1,t1)
  & P[s1,t1];
  hence thesis by A1;
end;

scheme
  Gen299{A,B,C() -> set, F(set,set) -> Element of C(), P[set, set], Q[set] } :
  { st1 where st1 is Element of C() :
    st1 in { F(s1,t1) where s1 is Element of A(), t1 is Element of B() :
       P[s1,t1] } & Q[st1] } =
  { F(s2,t2) where s2 is Element of A(), t2 is Element of B() :
    P[s2,t2] & Q[F(s2,t2)]}
proof
  thus { st1 where st1 is Element of C() : st1 in { F(s1,t1) where s1 is (
  Element of A()), t1 is Element of B() : P[s1,t1] } & Q[st1] } c= { F(s2,t2)
  where s2 is (Element of A()), t2 is Element of B() : P[s2,t2] & Q[F(s2,t2)]}
  proof
    let x be set;
    assume x in { st1 where st1 is Element of C() : st1 in { F(s1,t1) where
    s1 is (Element of A()), t1 is Element of B() : P[s1,t1] } & Q[st1] };
    then consider st1 being Element of C() such that
A1: x = st1 and
A2: st1 in { F(s1,t1) where s1 is (Element of A()), t1 is Element of B
    () : P[s1,t1] } and
A3: Q[st1];
    ex s1 being (Element of A()), t1 being Element of B() st st1 = F(s1,t1
    ) & P[s1,t1] by A2;
    hence thesis by A1,A3;
  end;
  let x be set;
  assume x in { F(s2,t2) where s2 is (Element of A()), t2 is Element of B() :
  P[s2,t2] & Q[F(s2,t2)]};
  then consider s2 being (Element of A()), t2 being Element of B() such that
A4: x = F(s2,t2) and
A5: P[s2,t2] and
A6: Q[F(s2,t2)];
  F(s2,t2) in { F(s1,t1) where s1 is (Element of A()), t1 is Element of B
  ( ) : P[s1,t1] } by A5;
  hence thesis by A4,A6;
end;

scheme
  Gen39{A() -> set, F(set) -> set, P[set], Q[set] } : { F(s) where s
is Element of A() : s in { s1 where s1 is Element of A(): Q[s1] } & P[s] } = {
  F(s2) where s2 is Element of A() : Q[s2] & P[s2] } proof
  defpred QQ[set] means Q[$1] & P[$1];
  defpred PP[set] means $1 in { s1 where s1 is Element of A(): Q[s1] } & P[$1];
A1: for s being Element of A() holds PP[s] iff QQ[s]
  proof
    let s be Element of A();
    now
      assume s in { s1 where s1 is Element of A(): Q[s1] };
      then ex s1 being Element of A() st s = s1 & Q[s1];
      hence Q[s];
    end;
    hence thesis;
  end;
  thus { F(s) where s is Element of A() : PP[s] } = { F(s2) where s2 is
  Element of A() : QQ[s2] } from Fraenkel69(A1);
end;

scheme
  Gen399{A,B() -> set, F(set,set) -> set, P[set,
set], Q[set] } : { F(s,t) where s is (Element of A()), t is Element of B() : s
in { s1 where s1 is Element of A(): Q[s1] } & P[s,t] } = { F(s2,t2) where s2 is
  (Element of A()), t2 is Element of B() : Q[s2] & P[s2,t2] } proof
  defpred QQ[set,set] means Q[$1] & P[$1,$2];
  defpred PP[set,set] means $1 in { s1 where s1 is Element of A(): Q[s1] } & P
  [$1,$2];
A1: for s being Element of A(), t being Element of B() holds PP[s,t] iff QQ[
  s,t]
  proof
    let s be Element of A(), t be Element of B();
    now
      assume s in { s1 where s1 is Element of A(): Q[s1] };
      then ex s1 being Element of A() st s = s1 & Q[s1];
      hence Q[s];
    end;
    hence thesis;
  end;
  thus { F(s,t) where s is (Element of A()), t is Element of B() : PP[s,t] } =
  { F(s2,t2) where s2 is (Element of A()), t2 is Element of B() : QQ[s2,t2] }
  from Fraenkel699(A1);
end;

scheme
  Gen499{A,B() -> set, F(set,set) -> set, P[set,
set], Q[set,set] } : { F(s,t) where s is (Element of A()), t is Element of B()
: P[s,t] } c= { F(s1,t1) where s1 is (Element of A()), t1 is Element of B() : Q
  [s1,t1] }
provided
A1: for s being (Element of A()), t being Element of B() st P[s,t] ex s9
being Element of A() st Q[s9,t] & F(s,t) = F(s9,t)
proof
  let x be set;
  assume
  x in { F(s,t) where s is (Element of A()), t is Element of B() : P[s ,t] };
  then consider s being (Element of A()), t being Element of B() such that
A2: x = F(s,t) and
A3: P[s,t];
  ex s9 being Element of A() st Q[s9,t] & F(s,t) = F(s9,t) by A1,A3;
  hence thesis by A2;
end;

scheme
  FrSet1{ D,A() -> set, P[set], F(set) -> set }:
  { F(y) where y is Element of D() : F(y) in A() & P[y] } c= A()
proof
  let x be set;
  assume x in { F(y) where y is Element of D() : F(y) in A() & P[y] };
  then ex y being Element of D() st x = F(y) & F(y) in A() & P[y];
  hence thesis;
end;

scheme
  FrSet2{ D,A() -> set, Q[set], F(set) -> set }:
  { F(y) where y is Element of D() : Q[y] & not F(y) in A() } misses A()
proof
  assume
  { F(y) where y is Element of D() : Q[y] & not F(y) in A() } meets A( );
  then consider x be set such that
A1: x in { F(y) where y is Element of D() : Q[y] & not F(y) in A() } and
A2: x in A() by XBOOLE_0:3;
  ex y being Element of D() st x = F(y) & Q[y] & not F(y) in A() by A1;
  hence thesis by A2;
end;

scheme
  FrEqua1{ A,B() -> set, F(set,set) -> set, x()
-> (Element of B()), P[set,set], Q[set,set] }: { F(s,t) where s is (Element of
A()), t is Element of B(): Q[s,t] } = { F(s9,x()) where s9 is Element of A(): P
  [s9,x()] }
provided
A1: for s being Element of A() for t being Element of B() holds Q[s,t]
iff t = x() & P[s,t]
proof
  thus { F(s,t) where s is (Element of A()), t is Element of B(): Q[s,t] } c=
  { F(s9,x()) where s9 is Element of A(): P[s9,x()] }
  proof
    let x be set;
    assume
    x in { F(s,t) where s is (Element of A()), t is Element of B(): Q[ s,t ] };
    then consider s being (Element of A()), t being Element of B() such that
A2: x = F(s,t) and
A3: Q[s,t];
A4: P[s,t] by A1,A3;
    t = x() by A1,A3;
    hence thesis by A2,A4;
  end;
  let x be set;
  assume x in { F(s9,x()) where s9 is Element of A(): P[s9,x()] };
  then consider s9 being Element of A() such that
A5: x = F(s9,x()) and
A6: P[s9,x()];
  Q[s9,x()] by A1,A6;
  hence thesis by A5;
end;

scheme
  FrEqua2{ A,B() -> set, F(set,set) -> set, x()
  -> (Element of B()), P[set,set] }: { F(s,t) where s is (Element of A()), t is
Element of B(): t = x() & P[s,t] } = { F(s9,x()) where s9 is Element of A(): P[
  s9,x()] } proof
  defpred Q[set,set] means $2 = x() & P[$1,$2];
A1: for s being Element of A() for t being Element of B() holds Q[s,t] iff t
  = x() & P[s,t];
  thus { F(s,t) where s is Element of A(), t is Element of B(): Q[s,t] } = { F
  (s9,x()) where s9 is Element of A(): P[s9,x()] } from FrEqua1(A1);
end;

:: dziedziny funkcji

reserve phi for Element of Funcs(A,B);

theorem Th4:
  for X,Y being set st Funcs(X,Y) <> {} & X c= A & Y c= B for f
  being Element of Funcs(X,Y) ex phi being Element of Funcs(A,B) st phi|X = f
proof
  let X,Y be set such that
A1: Funcs(X,Y) <> {} and
A2: X c= A and
A3: Y c= B;
  let f be Element of Funcs(X,Y);
  reconsider f9=f as PartFunc of A,B by A1,A2,A3,Th3;
  consider phi being Function of A,B such that
A4: for x st x in dom f9 holds phi.x = f9.x by FUNCT_2:71;
  reconsider phi as Element of Funcs(A,B) by FUNCT_2:8;
  take phi;
  ex g being Function st f = g & dom g = X & rng g c= Y by A1,FUNCT_2:def 2;
  then dom f9 = A /\ X by XBOOLE_1:28
    .= dom phi /\ X by FUNCT_2:def 1;
  hence thesis by A4,FUNCT_1:46;
end;

theorem Th5:
  phi|X = phi|(A /\ X)
proof
  dom phi = A by FUNCT_2:def 1;
  then
A1: dom (phi|X) = (dom phi /\ A) /\ X by RELAT_1:61
    .= dom phi /\ (A /\ X) by XBOOLE_1:16;
  for x st x in dom (phi|X) holds (phi|X).x = phi.x by FUNCT_1:47;
  hence thesis by A1,FUNCT_1:46;
end;

:: Zbiory skonczone

scheme
  FraenkelFin { A() -> set, X() -> set, F(set) -> set }:
  { F(w) where w is Element of A(): w in X() } is finite
provided
A1: X() is finite
proof
  set M = { F(w) where w is Element of A(): w in X() };
  per cases;
  suppose
A2: A() is empty;
    M c= {F({})}
    proof
      let x;
      assume x in M;
      then consider w being Element of A() such that
A3:   x = F(w) & w in X();
      w = {} by A2,SUBSET_1:def 1;
      hence thesis by A3,TARSKI:def 1;
    end;
    hence thesis;
  end;
  suppose
A4: A() is non empty;
  consider f being Function such that
A5: dom f = X() /\ A() and
A6: for y being set st y in X() /\ A() holds f.y = F(y) from FUNCT_1:sch 3;
  M = f.:X()
  proof
    thus M c= f.:X()
    proof
      let x be set;
      assume x in M;
      then consider u being Element of A() such that
A7:   x = F(u) and
A8:   u in X();
A9:   u in dom f by A4,A5,A8,XBOOLE_0:def 4;
      then f.u = F(u) by A5,A6;
      hence thesis by A7,A8,A9,FUNCT_1:def 6;
    end;
    let x be set;
    assume x in f.:X();
    then consider y being set such that
A10: y in dom f and
A11: y in X() and
A12: x = f.y by FUNCT_1:def 6;
    reconsider y as Element of A() by A5,A10,XBOOLE_0:def 4;
    x = F(y) by A5,A6,A10,A12;
    hence thesis by A11;
  end;
  hence thesis by A1;
  end;
end;

scheme
  CartFin { A, B() -> non empty set, X, Y() -> set, F(set, set) -> set }:
  { F(u,v) where u is Element of A(), v is Element of B() :
    u in X() & v in Y () } is finite
provided
A1: X() is finite and
A2: Y() is finite
proof
  deffunc G(set) = F($1`1,$1`2);
  set M = { F(u9,v9) where u9 is (Element of A()), v9 is Element of B() : u9
  in X() & v9 in Y() };
  consider f being Function such that
A3: dom f = [:X() /\ A(), Y() /\ B():] and
A4: for y being set st y in [:X() /\ A(), Y() /\ B():] holds f.y = G(y)
  from FUNCT_1:sch 3;
A5: dom f = [:X(), Y():] /\ [:A(), B():] by A3,ZFMISC_1:100;
  M = f.:[:X(), Y():]
  proof
    thus M c= f.:[:X(), Y():]
    proof
      let x be set;
      assume x in M;
      then consider u being Element of A(), v being Element of B() such that
A6:   x = F(u,v) and
A7:   u in X() and
A8:   v in Y();
A9:   [u,v] in [:X(), Y():] by A7,A8,ZFMISC_1:87;
      then
A10:  [u,v] in dom f by A5,XBOOLE_0:def 4;
A11:  [u,v]`2 = v;
      [u,v]`1 = u;
      then f.(u,v) = F(u,v) by A3,A4,A10,A11;
      hence thesis by A6,A9,A10,FUNCT_1:def 6;
    end;
    let x be set;
    assume x in f.:[:X(), Y():];
    then consider y being set such that
A12: y in dom f and
A13: y in [:X(), Y():] and
A14: x = f.y by FUNCT_1:def 6;
    reconsider y as Element of [:A(), B():] by A5,A12,XBOOLE_0:def 4;
A15: y = [y`1,y`2] by MCART_1:21;
    then
A16: y`1 in X() by A13,ZFMISC_1:87;
A17: y`2 in Y() by A13,A15,ZFMISC_1:87;
    x = F(y`1,y`2) by A3,A4,A12,A14;
    hence thesis by A16,A17;
  end;
  hence thesis by A1,A2;
end;

scheme
  Finiteness { A()->non empty set, B()->(Element of Fin A()), P[(Element of A(
  )), Element of A()] } : for x being Element of A() st x in B() ex y being
Element of A() st y in B() & P[y,x] & for z being Element of A() st z in B() &
  P[z,y] holds P[y,z]
provided
A1: for x being Element of A() holds P[x,x] and
A2: for x,y,z being Element of A() st P[x,y] & P[y,z] holds P[x,z]
proof
  defpred R[(Element of A()), Element of Fin A()] means ex y being Element of
A() st y in $2 & P[y,$1] & for z being Element of A() st z in $2 & P[z,y] holds
  P[y,z];
  defpred Q[Element of Fin A()] means for x being Element of A() st x in $1
  holds R[x, $1];
A3: now
    let B be (Element of Fin A()), x be Element of A();
    assume
A4: Q[B];
    thus Q[B \/ {.x.}]
    proof
      let z be Element of A() such that
A5:   z in B \/ {x};
      now
        per cases by A5,ZFMISC_1:136;
        suppose
          z in B;
          then consider y being Element of A() such that
A6:       y in B and
A7:       P[y,z] and
A8:       for x being Element of A() st x in B & P[x,y] holds P[y,x] by A4;
          now
            per cases;
            case
A9:           P[x,y];
              thus x in B \/ {x} by ZFMISC_1:136;
              thus P[x,z] by A2,A7,A9;
              let v be Element of A() such that
A10:          v in B \/ {x} and
A11:          P[v,x];
A12:          now
                assume
A13:            v in B;
                P[v,y] by A2,A9,A11;
                then P[y,v] by A8,A13;
                hence P[x,v] by A2,A9;
              end;
              v in B or v = x by A10,ZFMISC_1:136;
              hence P[x,v] by A1,A12;
            end;
            case
A14:          not P[x,y];
              thus y in B \/ {x} by A6,XBOOLE_0:def 3;
              thus P[y,z] by A7;
              let v be Element of A() such that
A15:          v in B \/ {x} and
A16:          P[v,y];
              v in B or v = x by A15,ZFMISC_1:136;
              hence P[y,v] by A8,A14,A16;
            end;
          end;
          hence thesis;
        end;
        suppose
A17:      z = x;
          now
            per cases;
            case
              ex w being Element of A() st w in B & P[w,x];
              then consider w being Element of A() such that
A18:          w in B and
A19:          P[w,z] by A17;
              consider y being Element of A() such that
A20:          y in B and
A21:          P[y,w] and
A22:          for x being Element of A() st x in B & P[x,y] holds P[y
              ,x] by A4,A18;
              take u = y;
              thus u in B \/ {x} by A20,XBOOLE_0:def 3;
              thus P[u,z] by A2,A19,A21;
              let v be Element of A() such that
A23:          v in B \/ {x} and
A24:          P[v,u];
              v in B or v = x by A23,ZFMISC_1:136;
              hence P[u,v] by A2,A17,A19,A21,A22,A24;
            end;
            case
A25:          for w being Element of A() st w in B holds not P[w,x];
              thus x in B \/ {x} by ZFMISC_1:136;
              thus
A26:          P[x,x] by A1;
              let v be Element of A() such that
A27:          v in B \/ {x} and
A28:          P[v,x];
              not v in B by A25,A28;
              hence P[x,v] by A26,A27,ZFMISC_1:136;
            end;
          end;
          hence thesis by A17;
        end;
      end;
      hence thesis;
    end;
  end;
A29: Q[{}.A()];
  for B being Element of Fin A() holds Q[B] from SETWISEO:sch 4(A29,A3 );
  hence thesis;
end;

scheme
  FinIm{A,B()->non empty set, x()-> (Element of Fin B()), F
  (set)->(Element of A()), P[set,set]}: ex c1 being Element of Fin A() st for t
being Element of A() holds t in c1 iff ex t9 being Element of B() st t9 in x()
  & t = F(t9) & P[t,t9] proof
  defpred R[set] means ex t9 being Element of B() st t9 in x() & $1 = F(t9) &
  P[$1,t9];
  set c = { F(t9) where t9 is Element of B() : t9 in x() }, c1 = { tt where tt
  is Element of A() : R[tt]};
A1: c1 c= c
  proof
    let x;
    assume x in c1;
    then ex tt being Element of A() st x = tt & ex t9 being Element of B() st
    t9 in x() & tt = F(t9) & P[tt,t9];
    hence thesis;
  end;
A2: c1 c= A() from FrSet0;
A3: x() is finite;
  c is finite from FraenkelFin(A3);
  then reconsider c1 as Element of Fin A() by A1,A2,FINSUB_1:def 5;
  take c1;
  let t be Element of A();
  t in c1 implies ex tt being Element of A() st t = tt & ex t9 being
  Element of B() st t9 in x() & tt = F(t9) & P[tt,t9];
  hence thesis;
end;

registration
  let A, B be finite set;
  cluster Funcs(A,B) -> finite;
  coherence
  proof
    bool [:A,B:] is finite;
    hence thesis by Th2,FINSET_1:1;
  end;
end;

theorem
  for A,B being set st A is finite & B is finite holds Funcs(A,B) is finite;

scheme
  ImFin { A() -> set, B() -> non empty set, X() -> set, Y() -> set,
F(set) -> set } : { F(phi9) where phi9 is Element of Funcs(A(),B()): phi9.:X()
  c= Y() } is finite
provided
A1: X() is finite and
A2: Y() is finite and
A3: for phi,psi being Element of Funcs(A(),B()) holds phi|X() = psi|X()
implies F(phi) = F(psi)
proof
  defpred P[set,set] means for phi being Element of Funcs(A(),B()) st phi|X()
  = $1 holds $2 = F(phi);
  set Z = { F(phi9) where phi9 is Element of Funcs(A(),B()): phi9.: X() c= Y()
  };
  set x = the Element of Z;
A4: B() /\ Y() c= B() by XBOOLE_1:17;
  assume
A5: not thesis;
  then Z <> {};
  then x in Z;
  then consider phi being Element of Funcs(A(),B()) such that
  x = F(phi) and
A6: phi.:X() c= Y();
  now
    assume B() /\ Y() = {};
    then
A7: phi.:X() = {} by A6,XBOOLE_1:3,19;
    A() = dom phi by FUNCT_2:def 1;
    then A() misses X() by A7,RELAT_1:118;
    hence A() /\ X() = {} by XBOOLE_0:def 7;
  end;
  then reconsider FF = Funcs(A() /\ X(),B() /\ Y()), Z as non empty set by A5,
FUNCT_2:8;
A8: B() /\ Y() c= Y() by XBOOLE_1:17;
A9: A() /\ X() c= A() by XBOOLE_1:17;
A10: now
    let f be Element of FF;
    consider phi being Element of Funcs(A(),B()) such that
A11: phi|(A() /\ X()) = f by A9,A4,Th4;
A12: phi|X() = f by A11,Th5;
    ex g being Function st f = g & dom g = A() /\ X() & rng g c= B() /\ Y
    () by FUNCT_2:def 2;
    then rng (phi|X()) c= Y() by A8,A12,XBOOLE_1:1;
    then phi.:X() c= Y() by RELAT_1:115;
    then F(phi) in Z;
    then reconsider g9 = F(phi) as Element of Z;
    take g = g9;
    thus P[f,g] by A3,A12;
  end;
  consider F being Function of FF, Z such that
A13: for f being Element of FF holds P[f,F.f] from FUNCT_2:sch 3(A10);
  Z c= F.:Funcs(A() /\ X(), B() /\ Y())
  proof
    let y be set;
    assume y in Z;
    then consider phi being Element of Funcs(A(),B()) such that
A14: y = F(phi) and
A15: phi.:X() c= Y();
    rng (phi|X()) c= Y() by A15,RELAT_1:115;
    then
A16: rng (phi|X()) c= B() /\ Y() by XBOOLE_1:19;
A17: dom (phi|X()) = dom phi /\ X() by RELAT_1:61
      .= A() /\ X() by FUNCT_2:def 1;
    then reconsider
x = phi|X() as Element of Funcs(A() /\ X(), B() /\ Y()) by A16,FUNCT_2:def 2;
    phi|X() in Funcs(A() /\ X(), B() /\ Y()) by A17,A16,FUNCT_2:def 2;
    then
A18: x in dom F by FUNCT_2:def 1;
    y = F.x by A13,A14;
    hence thesis by A18,FUNCT_1:def 6;
  end;
  hence contradiction by A1,A2,A5;
end;

:: Schematy zwiazane z pewnikiem wyboru

scheme
  FunctChoice { A()->non empty set, B()->non empty set, P[(Element of A()),
Element of B()], x()->Element of Fin A() }: ex ff being Function of A(), B() st
  for t being Element of A() st t in x() holds P[t,ff.t]
provided
A1: for t being Element of A() st t in x() ex ff being Element of B() st
P[t,ff]
proof
  set b = the Element of B();
  set M = { { ff where ff is Element of B() : P[tt,ff] } where tt is Element
  of A() : tt in x() };
  set f = the Function of A(), B();
  assume
A2: not thesis;
  then consider t being Element of A() such that
A3: t in x() and
  not P[t,f.t];
  { ff where ff is Element of B() : P[t,ff] } in M by A3;
  then reconsider M as non empty set;
  now
    let X;
    assume X in M;
    then consider t being Element of A() such that
A4: X = { ff where ff is Element of B() : P[t,ff] } and
A5: t in x();
    consider ff being Element of B() such that
A6: P[t,ff] by A1,A5;
    ff in X by A4,A6;
    hence X <> {};
  end;
  then consider Choice being Function such that
  dom Choice = M and
A7: X in M implies Choice.X in X by FUNCT_1:111;
  defpred Q[(Element of A()),set] means ($1 in x() implies $2 = Choice.{ ff
  where ff is Element of B() : P[$1,ff] }) & ($1 in x() or $2 = b);
A8: now
    let t be Element of A();
A9: now
      set s = { ff where ff is Element of B() : P[t,ff] };
      assume t in x();
      then s in M;
      then Choice.s in s by A7;
      then ex ff being Element of B() st Choice.s = ff & P[t,ff];
      hence Choice.s is Element of B();
    end;
    t in x() implies t in x();
    hence ex y being Element of B() st Q[t,y] by A9;
  end;
  consider f being Function of A(), B() such that
A10: for x being Element of A() holds Q[x,f.x] from FUNCT_2:sch 3(A8);
  now
    let t be Element of A();
    assume
A11: t in x();
    then
A12: { ff where ff is Element of B() : P[t,ff] } in M;
    f.t = Choice.{ ff where ff is Element of B() : P[t,ff] } by A10,A11;
    then f.t in { ff where ff is Element of B() : P[t,ff] } by A7,A12;
    then ex ff being Element of B() st f.t = ff & P[t,ff];
    hence P[t,f.t];
  end;
  hence contradiction by A2;
end;

scheme
  FuncsChoice { A()->non empty set, B()->non empty set, P[Element of A(),
Element of B()], x()->Element of Fin A() }: ex ff being Element of Funcs(A(),B(
  )) st for t being Element of A() st t in x() holds P[t,ff.t]
provided
A1: for t being Element of A() st t in x() ex ff being Element of B() st
P[t,ff]
proof
A2: for t being Element of A() st t in x() ex ff being Element of B() st P[t
  ,ff] by A1;
  consider ff being Function of A(), B() such that
A3: for t being Element of A() st t in x() holds P[t,ff.t] from
  FunctChoice(A2);
  reconsider ff as Element of Funcs(A(),B()) by FUNCT_2:8;
  take ff;
  thus thesis by A3;
end;

scheme
  FraenkelFin9 { A,B() -> non empty set, X() -> set, P[set,set] }: { x where x
  is Element of B(): ex w being Element of A() st P[w,x] & w in X() } is finite
provided
A1: X() is finite and
A2: for w being Element of A(), x,y being Element of B() st P[w,x] & P[w
,y] holds x = y
proof
  set M = { x where x is Element of B(): ex w being Element of A() st P[w,x] &
  w in X() };
  defpred Q[set,set] means P[$1,$2] & $1 in X() & $2 in B();
A3: for x,y being set st x in A() & Q[x,y] holds y in B();
A4: for x,y1,y2 being set st x in A() & Q[x,y1] & Q[x,y2] holds y1 = y2 by A2;
  consider f being PartFunc of A(),B() such that
A5: for x holds x in dom f iff x in A() & ex y being set st Q[x,y] and
A6: for x st x in dom f holds Q[x,f.x] from PARTFUN1:sch 2(A3,A4);
  M = f.:X()
  proof
    thus M c= f.:X()
    proof
      let x be set;
      assume x in M;
      then consider u being Element of B() such that
A7:   x = u and
A8:   ex w being Element of A() st P[w,u] & w in X();
      consider w being Element of A() such that
A9:   P[w,u] and
A10:  w in X() by A8;
A11:  w in dom f by A5,A9,A10;
      then Q[w,f.w] by A6;
      then f.w = x by A2,A7,A9;
      hence thesis by A10,A11,FUNCT_1:def 6;
    end;
    let x be set;
    assume x in f.:X();
    then consider y being set such that
A12: y in dom f and
A13: y in X() and
A14: x = f.y by FUNCT_1:def 6;
    reconsider x as Element of B() by A6,A12,A14;
    P[y,x] by A6,A12,A14;
    hence thesis by A12,A13;
  end;
  hence thesis by A1;
end;