The abstract of the Mizar article:

Predicate Calculus for Boolean Valued Functions. Part XII

by

Shunichi Kobayashi

Received December 28, 1999

MML identifier: BVFUNC24

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_2, MARGREL1, PARTIT1, EQREL_1, BVFUNC_2, BOOLE, SETFAM_1,
      CAT_1, FUNCT_4, RELAT_1, FUNCT_1, CANTOR_1, T_1TOPSP, TARSKI;
 notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1,
      FUNCT_1, FRAENKEL, CQC_LANG, FUNCT_4, MARGREL1, EQREL_1, PARTIT1,
      CANTOR_1, BVFUNC_1, BVFUNC_2;
 constructors BVFUNC_2, SETWISEO, CANTOR_1, FUNCT_7, BVFUNC_1;
 clusters SUBSET_1, PARTIT1, CQC_LANG, MARGREL1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin :: Chap. 1  Preliminaries

reserve Y for non empty set,

        G for Subset of PARTITIONS(Y),
        A, B, C, D, E, F, J, M for a_partition of Y,
        x,x1,x2,x3,x4,x5,x6,x7,x8,x9,y,X for set;

theorem :: BVFUNC24:1
 G={A,B,C,D,E,F,J} &
A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & B<>C & B<>D & B<>E & B<>F & B<>J &
C<>D & C<>E & C<>F & C<>J & D<>E & D<>F & D<>J & E<>F & E<>J & F<>J
implies
CompF(A,G) = B '/\' C '/\' D '/\' E '/\' F '/\' J;

theorem :: BVFUNC24:2
 G={A,B,C,D,E,F,J} &
A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & B<>C & B<>D & B<>E & B<>F & B<>J &
C<>D & C<>E & C<>F & C<>J & D<>E & D<>F & D<>J & E<>F & E<>J & F<>J
implies
CompF(B,G) = A '/\' C '/\' D '/\' E '/\' F '/\' J;

theorem :: BVFUNC24:3
 G={A,B,C,D,E,F,J} &
A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & B<>C & B<>D & B<>E & B<>F & B<>J &
C<>D & C<>E & C<>F & C<>J & D<>E & D<>F & D<>J & E<>F & E<>J & F<>J
implies
CompF(C,G) = A '/\' B '/\' D '/\' E '/\' F '/\' J;

theorem :: BVFUNC24:4
 G={A,B,C,D,E,F,J} &
A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & B<>C & B<>D & B<>E & B<>F & B<>J &
C<>D & C<>E & C<>F & C<>J & D<>E & D<>F & D<>J & E<>F & E<>J & F<>J
implies
CompF(D,G) = A '/\' B '/\' C '/\' E '/\' F '/\' J;

theorem :: BVFUNC24:5
 G={A,B,C,D,E,F,J} &
A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & B<>C & B<>D & B<>E & B<>F & B<>J &
C<>D & C<>E & C<>F & C<>J & D<>E & D<>F & D<>J & E<>F & E<>J & F<>J
implies
CompF(E,G) = A '/\' B '/\' C '/\' D '/\' F '/\' J;

theorem :: BVFUNC24:6
 G={A,B,C,D,E,F,J} &
A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & B<>C & B<>D & B<>E & B<>F & B<>J &
C<>D & C<>E & C<>F & C<>J & D<>E & D<>F & D<>J & E<>F & E<>J & F<>J
implies
CompF(F,G) = A '/\' B '/\' C '/\' D '/\' E '/\' J;

theorem :: BVFUNC24:7
   G={A,B,C,D,E,F,J} &
A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & B<>C & B<>D & B<>E & B<>F & B<>J &
C<>D & C<>E & C<>F & C<>J & D<>E & D<>F & D<>J & E<>F & E<>J & F<>J
implies
CompF(J,G) = A '/\' B '/\' C '/\' D '/\' E '/\' F;

theorem :: BVFUNC24:8
for A,B,C,D,E,F,J being set,
h being Function, A',B',C',D',E',F',J' being set st
A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & B<>C & B<>D & B<>E & B<>F & B<>J &
C<>D & C<>E & C<>F & C<>J & D<>E & D<>F & D<>J & E<>F & E<>J & F<>J &
h = (B .--> B') +* (C .--> C') +* (D .--> D') +*
    (E .--> E') +* (F .--> F') +* (J .--> J') +*
    (A .--> A')
holds h.A = A' & h.B = B' & h.C = C' &
      h.D = D' & h.E = E' & h.F = F' &
      h.J = J';

theorem :: BVFUNC24:9
for A,B,C,D,E,F,J being set,
h being Function, A',B',C',D',E',F',J' being set st
h = (B .--> B') +* (C .--> C') +* (D .--> D') +*
    (E .--> E') +* (F .--> F') +* (J .--> J') +* (A .--> A')
holds dom h = {A,B,C,D,E,F,J};

theorem :: BVFUNC24:10
for A,B,C,D,E,F,J being set,
h being Function, A',B',C',D',E',F',J' being set st
h = (B .--> B') +* (C .--> C') +* (D .--> D') +*
    (E .--> E') +* (F .--> F') +* (J .--> J') +* (A .--> A')
holds rng h = {h.A,h.B,h.C,h.D,h.E,h.F,h.J};

theorem :: BVFUNC24:11
  for G being Subset of PARTITIONS(Y),
A,B,C,D,E,F,J being a_partition of Y, z,u being Element of Y,
h being Function
st G is independent & G={A,B,C,D,E,F,J} &
A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & B<>C & B<>D & B<>E & B<>F & B<>J &
C<>D & C<>E & C<>F & C<>J & D<>E & D<>F & D<>J & E<>F & E<>J & F<>J
holds
EqClass(u,B '/\' C '/\' D '/\' E '/\' F '/\' J) meets EqClass(z,A);

theorem :: BVFUNC24:12
  for G being Subset of PARTITIONS(Y),
A,B,C,D,E,F,J being a_partition of Y, z,u being Element of Y
st G is independent & G={A,B,C,D,E,F,J} &
A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & B<>C & B<>D & B<>E & B<>F & B<>J &
C<>D & C<>E & C<>F & C<>J & D<>E & D<>F & D<>J & E<>F & E<>J & F<>J &
EqClass(z,C '/\' D '/\' E '/\' F '/\' J)=
EqClass(u,C '/\' D '/\' E '/\' F '/\' J)
holds EqClass(u,CompF(A,G)) meets EqClass(z,CompF(B,G));

theorem :: BVFUNC24:13
 G={A,B,C,D,E,F,J,M} &
A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M &
B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & C<>D & C<>E & C<>F & C<>J & C<>M &
D<>E & D<>F & D<>J & D<>M & E<>F & E<>J & E<>M & F<>J & F<>M & J<>M
implies
CompF(A,G) = B '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M;

theorem :: BVFUNC24:14
 G={A,B,C,D,E,F,J,M} &
A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M &
B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & C<>D & C<>E & C<>F & C<>J & C<>M &
D<>E & D<>F & D<>J & D<>M & E<>F & E<>J & E<>M & F<>J & F<>M & J<>M
implies
CompF(B,G) = A '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M;

theorem :: BVFUNC24:15
 G={A,B,C,D,E,F,J,M} &
A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M &
B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & C<>D & C<>E & C<>F & C<>J & C<>M &
D<>E & D<>F & D<>J & D<>M & E<>F & E<>J & E<>M & F<>J & F<>M & J<>M
implies
CompF(C,G) = A '/\' B '/\' D '/\' E '/\' F '/\' J '/\' M;

theorem :: BVFUNC24:16
 G={A,B,C,D,E,F,J,M} &
A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M &
B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & C<>D & C<>E & C<>F & C<>J & C<>M &
D<>E & D<>F & D<>J & D<>M & E<>F & E<>J & E<>M & F<>J & F<>M & J<>M
implies
CompF(D,G) = A '/\' B '/\' C '/\' E '/\' F '/\' J '/\' M;

theorem :: BVFUNC24:17
 G={A,B,C,D,E,F,J,M} &
A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M &
B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & C<>D & C<>E & C<>F & C<>J & C<>M &
D<>E & D<>F & D<>J & D<>M & E<>F & E<>J & E<>M & F<>J & F<>M & J<>M
implies
CompF(E,G) = A '/\' B '/\' C '/\' D '/\' F '/\' J '/\' M;

theorem :: BVFUNC24:18
 G={A,B,C,D,E,F,J,M} &
A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M &
B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & C<>D & C<>E & C<>F & C<>J & C<>M &
D<>E & D<>F & D<>J & D<>M & E<>F & E<>J & E<>M & F<>J & F<>M & J<>M
implies
CompF(F,G) = A '/\' B '/\' C '/\' D '/\' E '/\' J '/\' M;

theorem :: BVFUNC24:19
 G={A,B,C,D,E,F,J,M} &
A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M &
B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & C<>D & C<>E & C<>F & C<>J & C<>M &
D<>E & D<>F & D<>J & D<>M & E<>F & E<>J & E<>M & F<>J & F<>M & J<>M
implies
CompF(J,G) = A '/\' B '/\' C '/\' D '/\' E '/\' F '/\' M;

theorem :: BVFUNC24:20
   G={A,B,C,D,E,F,J,M} &
A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M &
B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & C<>D & C<>E & C<>F & C<>J & C<>M &
D<>E & D<>F & D<>J & D<>M & E<>F & E<>J & E<>M & F<>J & F<>M & J<>M
implies
CompF(M,G) = A '/\' B '/\' C '/\' D '/\' E '/\' F '/\' J;

theorem :: BVFUNC24:21
for A,B,C,D,E,F,J,M being set, h being Function,
A',B',C',D',E',F',J',M' being set st
A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M &
B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & C<>D & C<>E & C<>F & C<>J & C<>M &
D<>E & D<>F & D<>J & D<>M & E<>F & E<>J & E<>M & F<>J & F<>M & J<>M &
h = (B .--> B') +* (C .--> C') +* (D .--> D') +*
    (E .--> E') +* (F .--> F') +* (J .--> J') +*
    (M .--> M') +* (A .--> A')
holds h.B = B' & h.C = C' &
      h.D = D' & h.E = E' & h.F = F' &
      h.J = J';

theorem :: BVFUNC24:22
for A,B,C,D,E,F,J,M being set, h being Function,
A',B',C',D',E',F',J',M' being set st
h = (B .--> B') +* (C .--> C') +* (D .--> D') +*
    (E .--> E') +* (F .--> F') +* (J .--> J') +*
    (M .--> M') +* (A .--> A')
holds dom h = {A,B,C,D,E,F,J,M};

theorem :: BVFUNC24:23
for A,B,C,D,E,F,J,M being set, h being Function,
A',B',C',D',E',F',J',M' being set st
h = (B .--> B') +* (C .--> C') +* (D .--> D') +*
    (E .--> E') +* (F .--> F') +* (J .--> J') +*
    (M .--> M') +* (A .--> A')
holds rng h = {h.A,h.B,h.C,h.D,h.E,h.F,h.J,h.M};

theorem :: BVFUNC24:24
  for a being Element of Funcs(Y,BOOLEAN),G being Subset of PARTITIONS(Y),
A,B,C,D,E,F,J,M being a_partition of Y
, z,u being Element of Y, h being Function
st G is independent & G={A,B,C,D,E,F,J,M} &
A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M &
B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & C<>D & C<>E & C<>F & C<>J & C<>M &
D<>E & D<>F & D<>J & D<>M & E<>F & E<>J & E<>M & F<>J & F<>M & J<>M
holds EqClass(u,B '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M) /\
      EqClass(z,A) <> {};

theorem :: BVFUNC24:25
  for a being Element of Funcs(Y,BOOLEAN),G being Subset of PARTITIONS(Y),
A,B,C,D,E,F,J,M being a_partition of Y
, z,u being Element of Y
st G is independent & G={A,B,C,D,E,F,J,M} &
A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M &
B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & C<>D & C<>E & C<>F & C<>J & C<>M &
D<>E & D<>F & D<>J & D<>M & E<>F & E<>J & E<>M & F<>J & F<>M & J<>M &
EqClass(z,C '/\' D '/\' E '/\' F '/\' J '/\' M)=
EqClass(u,C '/\' D '/\' E '/\' F '/\' J '/\' M)
holds EqClass(u,CompF(A,G)) meets EqClass(z,CompF(B,G));

scheme UI10
  {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10()->set,
   P[set,set,set,set,set,set,set,set,set,set]}:
  P[x1(),x2(),x3(),x4(),x5(),x6(),x7(),x8(),x9(),x10()]
provided
  for x1,x2,x3,x4,x5,x6,x7,x8,x9,x10 being set
         holds P[x1,x2,x3,x4,x5,x6,x7,x8,x9,x10];

definition
   let x1,x2,x3,x4,x5,x6,x7,x8,x9;
    func { x1,x2,x3,x4,x5,x6,x7,x8,x9 } -> set means
:: BVFUNC24:def 1
 x in it iff x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 or x=x7 or
                  x=x8 or x=x9;
end;

theorem :: BVFUNC24:26
      x in { x1,x2,x3,x4,x5,x6,x7,x8,x9 } implies
      x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 or x=x7 or x=x8
   or x=x9;

theorem :: BVFUNC24:27
 { x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1 } \/ { x2,x3,x4,x5,x6,x7,x8,x9 };

theorem :: BVFUNC24:28
 { x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2 } \/ { x3,x4,x5,x6,x7,x8,x9 };

theorem :: BVFUNC24:29
 { x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3 } \/ { x4,x5,x6,x7,x8,x9 };

theorem :: BVFUNC24:30
  { x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3,x4 } \/ { x5,x6,x7,x8,x9 }
;

theorem :: BVFUNC24:31
 { x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3,x4,x5 } \/ { x6,x7,x8,x9 };

theorem :: BVFUNC24:32
 { x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3,x4,x5,x6 } \/ { x7,x8,x9 };

theorem :: BVFUNC24:33
 { x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3,x4,x5,x6,x7 } \/ { x8,x9 };

theorem :: BVFUNC24:34
   { x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3,x4,x5,x6,x7,x8 } \/ { x9 };

theorem :: BVFUNC24:35
for G being Subset of PARTITIONS(Y),
A,B,C,D,E,F,J,M,N being a_partition of Y
st G={A,B,C,D,E,F,J,M,N} &
A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M & A<>N &
B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & B<>N &
C<>D & C<>E & C<>F & C<>J & C<>M & C<>N & D<>E & D<>F & D<>J & D<>M & D<>N &
E<>F & E<>J & E<>M & E<>N & F<>J & F<>M & F<>N & J<>M & J<>N & M<>N
holds
CompF(A,G) = B '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M '/\' N;

theorem :: BVFUNC24:36
for G being Subset of PARTITIONS(Y),
A,B,C,D,E,F,J,M,N being a_partition of Y
st G={A,B,C,D,E,F,J,M,N} &
A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M & A<>N &
B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & B<>N &
C<>D & C<>E & C<>F & C<>J & C<>M & C<>N & D<>E & D<>F & D<>J & D<>M & D<>N &
E<>F & E<>J & E<>M & E<>N & F<>J & F<>M & F<>N & J<>M & J<>N & M<>N
holds
CompF(B,G) = A '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M '/\' N;

theorem :: BVFUNC24:37
for G being Subset of PARTITIONS(Y),
A,B,C,D,E,F,J,M,N being a_partition of Y
st G={A,B,C,D,E,F,J,M,N} &
A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M & A<>N &
B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & B<>N &
C<>D & C<>E & C<>F & C<>J & C<>M & C<>N & D<>E & D<>F & D<>J & D<>M & D<>N &
E<>F & E<>J & E<>M & E<>N & F<>J & F<>M & F<>N & J<>M & J<>N & M<>N
holds
CompF(C,G) = A '/\' B '/\' D '/\' E '/\' F '/\' J '/\' M '/\' N;

theorem :: BVFUNC24:38
for G being Subset of PARTITIONS(Y),
A,B,C,D,E,F,J,M,N being a_partition of Y
st G={A,B,C,D,E,F,J,M,N} &
A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M & A<>N &
B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & B<>N &
C<>D & C<>E & C<>F & C<>J & C<>M & C<>N & D<>E & D<>F & D<>J & D<>M & D<>N &
E<>F & E<>J & E<>M & E<>N & F<>J & F<>M & F<>N & J<>M & J<>N & M<>N
holds
CompF(D,G) = A '/\' B '/\' C '/\' E '/\' F '/\' J '/\' M '/\' N;

theorem :: BVFUNC24:39
for G being Subset of PARTITIONS(Y),
A,B,C,D,E,F,J,M,N being a_partition of Y
st G={A,B,C,D,E,F,J,M,N} &
A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M & A<>N &
B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & B<>N &
C<>D & C<>E & C<>F & C<>J & C<>M & C<>N & D<>E & D<>F & D<>J & D<>M & D<>N &
E<>F & E<>J & E<>M & E<>N & F<>J & F<>M & F<>N & J<>M & J<>N & M<>N
holds
CompF(E,G) = A '/\' B '/\' C '/\' D '/\' F '/\' J '/\' M '/\' N;

theorem :: BVFUNC24:40
for G being Subset of PARTITIONS(Y),
A,B,C,D,E,F,J,M,N being a_partition of Y
st G={A,B,C,D,E,F,J,M,N} &
A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M & A<>N &
B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & B<>N &
C<>D & C<>E & C<>F & C<>J & C<>M & C<>N & D<>E & D<>F & D<>J & D<>M & D<>N &
E<>F & E<>J & E<>M & E<>N & F<>J & F<>M & F<>N & J<>M & J<>N & M<>N
holds
CompF(F,G) = A '/\' B '/\' C '/\' D '/\' E '/\' J '/\' M '/\' N;

theorem :: BVFUNC24:41
for G being Subset of PARTITIONS(Y),
A,B,C,D,E,F,J,M,N being a_partition of Y
st G={A,B,C,D,E,F,J,M,N} &
A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M & A<>N &
B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & B<>N &
C<>D & C<>E & C<>F & C<>J & C<>M & C<>N & D<>E & D<>F & D<>J & D<>M & D<>N &
E<>F & E<>J & E<>M & E<>N & F<>J & F<>M & F<>N & J<>M & J<>N & M<>N
holds
CompF(J,G) = A '/\' B '/\' C '/\' D '/\' E '/\' F '/\' M '/\' N;

theorem :: BVFUNC24:42
for G being Subset of PARTITIONS(Y),
A,B,C,D,E,F,J,M,N being a_partition of Y
st G={A,B,C,D,E,F,J,M,N} &
A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M & A<>N &
B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & B<>N &
C<>D & C<>E & C<>F & C<>J & C<>M & C<>N & D<>E & D<>F & D<>J & D<>M & D<>N &
E<>F & E<>J & E<>M & E<>N & F<>J & F<>M & F<>N & J<>M & J<>N & M<>N
holds
CompF(M,G) = A '/\' B '/\' C '/\' D '/\' E '/\' F '/\' J '/\' N;

theorem :: BVFUNC24:43
  for G being Subset of PARTITIONS(Y),
A,B,C,D,E,F,J,M,N being a_partition of Y
st G={A,B,C,D,E,F,J,M,N} &
A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M & A<>N &
B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & B<>N &
C<>D & C<>E & C<>F & C<>J & C<>M & C<>N & D<>E & D<>F & D<>J & D<>M & D<>N &
E<>F & E<>J & E<>M & E<>N & F<>J & F<>M & F<>N & J<>M & J<>N & M<>N
holds
CompF(N,G) = A '/\' B '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M;

theorem :: BVFUNC24:44
for A,B,C,D,E,F,J,M,N being set, h being Function,
A',B',C',D',E',F',J',M',N' being set st
A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M & A<>N &
B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & B<>N &
C<>D & C<>E & C<>F & C<>J & C<>M & C<>N & D<>E & D<>F & D<>J & D<>M & D<>N &
E<>F & E<>J & E<>M & E<>N & F<>J & F<>M & F<>N & J<>M & J<>N & M<>N &
h = (B .--> B') +* (C .--> C') +* (D .--> D') +*
    (E .--> E') +* (F .--> F') +* (J .--> J') +*
    (M .--> M') +* (N .--> N') +* (A .--> A')
holds h.A = A' & h.B = B' & h.C = C' &
      h.D = D' & h.E = E' & h.F = F' &
      h.J = J' & h.M = M' & h.N = N';

theorem :: BVFUNC24:45
for A,B,C,D,E,F,J,M,N being set, h being Function,
A',B',C',D',E',F',J',M',N' being set st
h = (B .--> B') +* (C .--> C') +* (D .--> D') +*
    (E .--> E') +* (F .--> F') +* (J .--> J') +*
    (M .--> M') +* (N .--> N') +* (A .--> A')
holds dom h = {A,B,C,D,E,F,J,M,N};

theorem :: BVFUNC24:46
for A,B,C,D,E,F,J,M,N being set, h being Function,
A',B',C',D',E',F',J',M',N' being set st
h = (B .--> B') +* (C .--> C') +* (D .--> D') +*
    (E .--> E') +* (F .--> F') +* (J .--> J') +*
    (M .--> M') +* (N .--> N') +* (A .--> A')
holds rng h = {h.A,h.B,h.C,h.D,h.E,h.F,h.J,h.M,h.N};

theorem :: BVFUNC24:47
  for a being Element of Funcs(Y,BOOLEAN),G being Subset of PARTITIONS(Y),
A,B,C,D,E,F,J,M,N being a_partition of Y
, z,u being Element of Y, h being Function
st G is independent & G={A,B,C,D,E,F,J,M,N} &
A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M & A<>N &
B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & B<>N &
C<>D & C<>E & C<>F & C<>J & C<>M & C<>N & D<>E & D<>F & D<>J & D<>M & D<>N &
E<>F & E<>J & E<>M & E<>N & F<>J & F<>M & F<>N & J<>M & J<>N & M<>N
holds EqClass(u,B '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M '/\' N) /\
      EqClass(z,A) <> {};

theorem :: BVFUNC24:48
  for a being Element of Funcs(Y,BOOLEAN),G being Subset of PARTITIONS(Y),
A,B,C,D,E,F,J,M,N being a_partition of Y, z,u being Element of Y
st G is independent & G={A,B,C,D,E,F,J,M,N} &
A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M & A<>N &
B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & B<>N &
C<>D & C<>E & C<>F & C<>J & C<>M & C<>N & D<>E & D<>F & D<>J & D<>M & D<>N &
E<>F & E<>J & E<>M & E<>N & F<>J & F<>M & F<>N & J<>M & J<>N & M<>N &
EqClass(z,C '/\' D '/\' E '/\' F '/\' J '/\' M '/\' N)=
EqClass(u,C '/\' D '/\' E '/\' F '/\' J '/\' M '/\' N)
holds EqClass(u,CompF(A,G)) meets EqClass(z,CompF(B,G));

theorem :: BVFUNC24:49
    x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 or x=x7 or x=x8 or x=x9
    implies x in { x1,x2,x3,x4,x5,x6,x7,x8,x9 };