:: Predicate Calculus for Boolean Valued Functions, { VI }
:: by Shunichi Kobayashi
::
:: Received October 19, 1999
:: Copyright (c) 1999-2012 Association of Mizar Users


begin

theorem Th1: :: BVFUNC14:1
for Y being non empty set
for z being Element of Y
for PA, PB being a_partition of Y holds EqClass (z,(PA '/\' PB)) = (EqClass (z,PA)) /\ (EqClass (z,PB))
proofend;

theorem :: BVFUNC14:2
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G = {A,B} &amp; A <> B holds
'/\' G = A '/\' B
proofend;

Lm1:  for B, C, D, b, c, d being set holds dom (((B .--> b) +* (C .--> c)) +* (D .--> d)) = {B,C,D}
proofend;

Lm2:  for f being Function
for C, D, c, d being set st C <> D holds
((f +* (C .--> c)) +* (D .--> d)) . C = c
proofend;

Lm3:  for B, C, D, b, c, d being set st B <> C &amp; D <> B holds
(((B .--> b) +* (C .--> c)) +* (D .--> d)) . B = b
proofend;

Lm4:  for B, C, D, b, c, d being set
for h being Function st h = ((B .--> b) +* (C .--> c)) +* (D .--> d) holds
rng h = {(h . B),(h . C),(h . D)}
proofend;

theorem :: BVFUNC14:3
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for B, C, D being a_partition of Y st G = {B,C,D} &amp; B <> C &amp; C <> D &amp; D <> B holds
'/\' G = (B '/\' C) '/\' D
proofend;

theorem Th4: :: BVFUNC14:4
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C being a_partition of Y st G = {A,B,C} &amp; A <> B &amp; C <> A holds
CompF (A,G) = B '/\' C
proofend;

theorem Th5: :: BVFUNC14:5
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C being a_partition of Y st G = {A,B,C} &amp; A <> B &amp; B <> C holds
CompF (B,G) = C '/\' A
proofend;

theorem :: BVFUNC14:6
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C being a_partition of Y st G = {A,B,C} &amp; B <> C &amp; C <> A holds
CompF (C,G) = A '/\' B
proofend;

theorem Th7: :: BVFUNC14:7
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D being a_partition of Y st G = {A,B,C,D} &amp; A <> B &amp; A <> C &amp; A <> D holds
CompF (A,G) = (B '/\' C) '/\' D
proofend;

theorem Th8: :: BVFUNC14:8
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D being a_partition of Y st G = {A,B,C,D} &amp; A <> B &amp; B <> C &amp; B <> D holds
CompF (B,G) = (A '/\' C) '/\' D
proofend;

theorem :: BVFUNC14:9
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D being a_partition of Y st G = {A,B,C,D} &amp; A <> C &amp; B <> C &amp; C <> D holds
CompF (C,G) = (A '/\' B) '/\' D
proofend;

theorem :: BVFUNC14:10
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D being a_partition of Y st G = {A,B,C,D} &amp; A <> D &amp; B <> D &amp; C <> D holds
CompF (D,G) = (A '/\' C) '/\' B
proofend;

theorem :: BVFUNC14:11
for B, C, D, b, c, d being set holds dom (((B .--> b) +* (C .--> c)) +* (D .--> d)) = {B,C,D} by Lm1;

theorem :: BVFUNC14:12
for f being Function
for C, D, c, d being set st C <> D holds
((f +* (C .--> c)) +* (D .--> d)) . C = c by Lm2;

theorem :: BVFUNC14:13
for B, C, D, b, c, d being set st B <> C &amp; D <> B holds
(((B .--> b) +* (C .--> c)) +* (D .--> d)) . B = b by Lm3;

theorem :: BVFUNC14:14
for B, C, D, b, c, d being set
for h being Function st h = ((B .--> b) +* (C .--> c)) +* (D .--> d) holds
rng h = {(h . B),(h . C),(h . D)} by Lm4;

:: from BVFUNC20
theorem Th15: :: BVFUNC14:15
for Y being non empty set
for A, B, C, D being a_partition of Y
for h being Function
for A9, B9, C9, D9 being set st A <> B &amp; A <> C &amp; A <> D &amp; B <> C &amp; B <> D &amp; C <> D &amp; h = (((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (A .--> A9) holds
( h . B = B9 &amp; h . C = C9 &amp; h . D = D9 )
proofend;

theorem Th16: :: BVFUNC14:16
for A, B, C, D being set
for h being Function
for A9, B9, C9, D9 being set st h = (((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (A .--> A9) holds
dom h = {A,B,C,D}
proofend;

theorem Th17: :: BVFUNC14:17
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D being a_partition of Y
for h being Function
for A9, B9, C9, D9 being set st G = {A,B,C,D} &amp; h = (((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (A .--> A9) holds
rng h = {(h . A),(h . B),(h . C),(h . D)}
proofend;

theorem :: BVFUNC14:18
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D being a_partition of Y
for z, u being Element of Y
for h being Function st G is independent &amp; G = {A,B,C,D} &amp; A <> B &amp; A <> C &amp; A <> D &amp; B <> C &amp; B <> D &amp; C <> D holds
EqClass (u,((B '/\' C) '/\' D)) meets EqClass (z,A)
proofend;

theorem :: BVFUNC14:19
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D being a_partition of Y
for z, u being Element of Y st G is independent &amp; G = {A,B,C,D} &amp; A <> B &amp; A <> C &amp; A <> D &amp; B <> C &amp; B <> D &amp; C <> D &amp; EqClass (z,(C '/\' D)) = EqClass (u,(C '/\' D)) holds
EqClass (u,(CompF (A,G))) meets EqClass (z,(CompF (B,G)))
proofend;

theorem :: BVFUNC14:20
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C being a_partition of Y
for z, u being Element of Y st G is independent &amp; G = {A,B,C} &amp; A <> B &amp; B <> C &amp; C <> A &amp; EqClass (z,C) = EqClass (u,C) holds
EqClass (u,(CompF (A,G))) meets EqClass (z,(CompF (B,G)))
proofend;

theorem Th21: :: BVFUNC14:21
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E being a_partition of Y st G = {A,B,C,D,E} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E holds
CompF (A,G) = ((B '/\' C) '/\' D) '/\' E
proofend;

theorem Th22: :: BVFUNC14:22
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E being a_partition of Y st G = {A,B,C,D,E} &amp; A <> B &amp; B <> C &amp; B <> D &amp; B <> E holds
CompF (B,G) = ((A '/\' C) '/\' D) '/\' E
proofend;

theorem Th23: :: BVFUNC14:23
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E being a_partition of Y st G = {A,B,C,D,E} &amp; A <> C &amp; B <> C &amp; C <> D &amp; C <> E holds
CompF (C,G) = ((A '/\' B) '/\' D) '/\' E
proofend;

theorem Th24: :: BVFUNC14:24
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E being a_partition of Y st G = {A,B,C,D,E} &amp; A <> D &amp; B <> D &amp; C <> D &amp; D <> E holds
CompF (D,G) = ((A '/\' B) '/\' C) '/\' E
proofend;

theorem :: BVFUNC14:25
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E being a_partition of Y st G = {A,B,C,D,E} &amp; A <> E &amp; B <> E &amp; C <> E &amp; D <> E holds
CompF (E,G) = ((A '/\' B) '/\' C) '/\' D
proofend;

theorem Th26: :: BVFUNC14:26
for A, B, C, D, E being set
for h being Function
for A9, B9, C9, D9, E9 being set st A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; B <> C &amp; B <> D &amp; B <> E &amp; C <> D &amp; C <> E &amp; D <> E &amp; h = ((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (A .--> A9) holds
( h . A = A9 &amp; h . B = B9 &amp; h . C = C9 &amp; h . D = D9 &amp; h . E = E9 )
proofend;

theorem Th27: :: BVFUNC14:27
for A, B, C, D, E being set
for h being Function
for A9, B9, C9, D9, E9 being set st h = ((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (A .--> A9) holds
dom h = {A,B,C,D,E}
proofend;

theorem Th28: :: BVFUNC14:28
for A, B, C, D, E being set
for h being Function
for A9, B9, C9, D9, E9 being set st h = ((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (A .--> A9) holds
rng h = {(h . A),(h . B),(h . C),(h . D),(h . E)}
proofend;

theorem :: BVFUNC14:29
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E being a_partition of Y
for z, u being Element of Y
for h being Function st G is independent &amp; G = {A,B,C,D,E} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; B <> C &amp; B <> D &amp; B <> E &amp; C <> D &amp; C <> E &amp; D <> E holds
EqClass (u,(((B '/\' C) '/\' D) '/\' E)) meets EqClass (z,A)
proofend;

theorem :: BVFUNC14:30
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E being a_partition of Y
for z, u being Element of Y st G is independent &amp; G = {A,B,C,D,E} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; B <> C &amp; B <> D &amp; B <> E &amp; C <> D &amp; C <> E &amp; D <> E &amp; EqClass (z,((C '/\' D) '/\' E)) = EqClass (u,((C '/\' D) '/\' E)) holds
EqClass (u,(CompF (A,G))) meets EqClass (z,(CompF (B,G)))
proofend;

:: moved from BVFUNC23, AG 4.01.2006
theorem Th31: :: BVFUNC14:31
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F being a_partition of Y st G = {A,B,C,D,E,F} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; C <> D &amp; C <> E &amp; C <> F &amp; D <> E &amp; D <> F &amp; E <> F holds
CompF (A,G) = (((B '/\' C) '/\' D) '/\' E) '/\' F
proofend;

theorem Th32: :: BVFUNC14:32
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F being a_partition of Y st G = {A,B,C,D,E,F} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; C <> D &amp; C <> E &amp; C <> F &amp; D <> E &amp; D <> F &amp; E <> F holds
CompF (B,G) = (((A '/\' C) '/\' D) '/\' E) '/\' F
proofend;

theorem Th33: :: BVFUNC14:33
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F being a_partition of Y st G = {A,B,C,D,E,F} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; C <> D &amp; C <> E &amp; C <> F &amp; D <> E &amp; D <> F &amp; E <> F holds
CompF (C,G) = (((A '/\' B) '/\' D) '/\' E) '/\' F
proofend;

theorem Th34: :: BVFUNC14:34
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F being a_partition of Y st G = {A,B,C,D,E,F} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; C <> D &amp; C <> E &amp; C <> F &amp; D <> E &amp; D <> F &amp; E <> F holds
CompF (D,G) = (((A '/\' B) '/\' C) '/\' E) '/\' F
proofend;

theorem Th35: :: BVFUNC14:35
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F being a_partition of Y st G = {A,B,C,D,E,F} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; C <> D &amp; C <> E &amp; C <> F &amp; D <> E &amp; D <> F &amp; E <> F holds
CompF (E,G) = (((A '/\' B) '/\' C) '/\' D) '/\' F
proofend;

theorem :: BVFUNC14:36
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F being a_partition of Y st G = {A,B,C,D,E,F} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; C <> D &amp; C <> E &amp; C <> F &amp; D <> E &amp; D <> F &amp; E <> F holds
CompF (F,G) = (((A '/\' B) '/\' C) '/\' D) '/\' E
proofend;

theorem Th37: :: BVFUNC14:37
for A, B, C, D, E, F being set
for h being Function
for A9, B9, C9, D9, E9, F9 being set st A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; C <> D &amp; C <> E &amp; C <> F &amp; D <> E &amp; D <> F &amp; E <> F &amp; h = (((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (A .--> A9) holds
( h . A = A9 &amp; h . B = B9 &amp; h . C = C9 &amp; h . D = D9 &amp; h . E = E9 &amp; h . F = F9 )
proofend;

theorem Th38: :: BVFUNC14:38
for A, B, C, D, E, F being set
for h being Function
for A9, B9, C9, D9, E9, F9 being set st h = (((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (A .--> A9) holds
dom h = {A,B,C,D,E,F}
proofend;

theorem Th39: :: BVFUNC14:39
for A, B, C, D, E, F being set
for h being Function
for A9, B9, C9, D9, E9, F9 being set st h = (((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (A .--> A9) holds
rng h = {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F)}
proofend;

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

theorem :: BVFUNC14:41
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F being a_partition of Y
for z, u being Element of Y
for h being Function st G is independent &amp; G = {A,B,C,D,E,F} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; C <> D &amp; C <> E &amp; C <> F &amp; D <> E &amp; D <> F &amp; E <> F &amp; EqClass (z,(((C '/\' D) '/\' E) '/\' F)) = EqClass (u,(((C '/\' D) '/\' E) '/\' F)) holds
EqClass (u,(CompF (A,G))) meets EqClass (z,(CompF (B,G)))
proofend;

begin

theorem Th42: :: BVFUNC14:42
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J being a_partition of Y st G = {A,B,C,D,E,F,J} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; A <> J &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; B <> J &amp; C <> D &amp; C <> E &amp; C <> F &amp; C <> J &amp; D <> E &amp; D <> F &amp; D <> J &amp; E <> F &amp; E <> J &amp; F <> J holds
CompF (A,G) = ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J
proofend;

theorem Th43: :: BVFUNC14:43
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J being a_partition of Y st G = {A,B,C,D,E,F,J} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; A <> J &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; B <> J &amp; C <> D &amp; C <> E &amp; C <> F &amp; C <> J &amp; D <> E &amp; D <> F &amp; D <> J &amp; E <> F &amp; E <> J &amp; F <> J holds
CompF (B,G) = ((((A '/\' C) '/\' D) '/\' E) '/\' F) '/\' J
proofend;

theorem Th44: :: BVFUNC14:44
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J being a_partition of Y st G = {A,B,C,D,E,F,J} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; A <> J &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; B <> J &amp; C <> D &amp; C <> E &amp; C <> F &amp; C <> J &amp; D <> E &amp; D <> F &amp; D <> J &amp; E <> F &amp; E <> J &amp; F <> J holds
CompF (C,G) = ((((A '/\' B) '/\' D) '/\' E) '/\' F) '/\' J
proofend;

theorem Th45: :: BVFUNC14:45
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J being a_partition of Y st G = {A,B,C,D,E,F,J} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; A <> J &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; B <> J &amp; C <> D &amp; C <> E &amp; C <> F &amp; C <> J &amp; D <> E &amp; D <> F &amp; D <> J &amp; E <> F &amp; E <> J &amp; F <> J holds
CompF (D,G) = ((((A '/\' B) '/\' C) '/\' E) '/\' F) '/\' J
proofend;

theorem Th46: :: BVFUNC14:46
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J being a_partition of Y st G = {A,B,C,D,E,F,J} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; A <> J &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; B <> J &amp; C <> D &amp; C <> E &amp; C <> F &amp; C <> J &amp; D <> E &amp; D <> F &amp; D <> J &amp; E <> F &amp; E <> J &amp; F <> J holds
CompF (E,G) = ((((A '/\' B) '/\' C) '/\' D) '/\' F) '/\' J
proofend;

theorem Th47: :: BVFUNC14:47
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J being a_partition of Y st G = {A,B,C,D,E,F,J} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; A <> J &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; B <> J &amp; C <> D &amp; C <> E &amp; C <> F &amp; C <> J &amp; D <> E &amp; D <> F &amp; D <> J &amp; E <> F &amp; E <> J &amp; F <> J holds
CompF (F,G) = ((((A '/\' B) '/\' C) '/\' D) '/\' E) '/\' J
proofend;

theorem :: BVFUNC14:48
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J being a_partition of Y st G = {A,B,C,D,E,F,J} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; A <> J &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; B <> J &amp; C <> D &amp; C <> E &amp; C <> F &amp; C <> J &amp; D <> E &amp; D <> F &amp; D <> J &amp; E <> F &amp; E <> J &amp; F <> J holds
CompF (J,G) = ((((A '/\' B) '/\' C) '/\' D) '/\' E) '/\' F
proofend;

theorem Th49: :: BVFUNC14:49
for A, B, C, D, E, F, J being set
for h being Function
for A9, B9, C9, D9, E9, F9, J9 being set st A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; A <> J &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; B <> J &amp; C <> D &amp; C <> E &amp; C <> F &amp; C <> J &amp; D <> E &amp; D <> F &amp; D <> J &amp; E <> F &amp; E <> J &amp; F <> J &amp; h = ((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (A .--> A9) holds
( h . A = A9 &amp; h . B = B9 &amp; h . C = C9 &amp; h . D = D9 &amp; h . E = E9 &amp; h . F = F9 &amp; h . J = J9 )
proofend;

theorem Th50: :: BVFUNC14:50
for A, B, C, D, E, F, J being set
for h being Function
for A9, B9, C9, D9, E9, F9, J9 being set st h = ((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (A .--> A9) holds
dom h = {A,B,C,D,E,F,J}
proofend;

theorem Th51: :: BVFUNC14:51
for A, B, C, D, E, F, J being set
for h being Function
for A9, B9, C9, D9, E9, F9, J9 being set st h = ((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (A .--> A9) holds
rng h = {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J)}
proofend;

theorem :: BVFUNC14:52
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J being a_partition of Y
for z, u being Element of Y st G is independent &amp; G = {A,B,C,D,E,F,J} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; A <> J &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; B <> J &amp; C <> D &amp; C <> E &amp; C <> F &amp; C <> J &amp; D <> E &amp; D <> F &amp; D <> J &amp; E <> F &amp; E <> J &amp; F <> J holds
EqClass (u,(((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J)) meets EqClass (z,A)
proofend;

theorem :: BVFUNC14:53
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J being a_partition of Y
for z, u being Element of Y st G is independent &amp; G = {A,B,C,D,E,F,J} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; A <> J &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; B <> J &amp; C <> D &amp; C <> E &amp; C <> F &amp; C <> J &amp; D <> E &amp; D <> F &amp; D <> J &amp; E <> F &amp; E <> J &amp; F <> J &amp; 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)))
proofend;

theorem Th54: :: BVFUNC14:54
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M being a_partition of Y st G = {A,B,C,D,E,F,J,M} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; A <> J &amp; A <> M &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; B <> J &amp; B <> M &amp; C <> D &amp; C <> E &amp; C <> F &amp; C <> J &amp; C <> M &amp; D <> E &amp; D <> F &amp; D <> J &amp; D <> M &amp; E <> F &amp; E <> J &amp; E <> M &amp; F <> J &amp; F <> M &amp; J <> M holds
CompF (A,G) = (((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M
proofend;

theorem Th55: :: BVFUNC14:55
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M being a_partition of Y st G = {A,B,C,D,E,F,J,M} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; A <> J &amp; A <> M &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; B <> J &amp; B <> M &amp; C <> D &amp; C <> E &amp; C <> F &amp; C <> J &amp; C <> M &amp; D <> E &amp; D <> F &amp; D <> J &amp; D <> M &amp; E <> F &amp; E <> J &amp; E <> M &amp; F <> J &amp; F <> M &amp; J <> M holds
CompF (B,G) = (((((A '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M
proofend;

theorem Th56: :: BVFUNC14:56
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M being a_partition of Y st G = {A,B,C,D,E,F,J,M} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; A <> J &amp; A <> M &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; B <> J &amp; B <> M &amp; C <> D &amp; C <> E &amp; C <> F &amp; C <> J &amp; C <> M &amp; D <> E &amp; D <> F &amp; D <> J &amp; D <> M &amp; E <> F &amp; E <> J &amp; E <> M &amp; F <> J &amp; F <> M &amp; J <> M holds
CompF (C,G) = (((((A '/\' B) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M
proofend;

theorem Th57: :: BVFUNC14:57
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M being a_partition of Y st G = {A,B,C,D,E,F,J,M} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; A <> J &amp; A <> M &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; B <> J &amp; B <> M &amp; C <> D &amp; C <> E &amp; C <> F &amp; C <> J &amp; C <> M &amp; D <> E &amp; D <> F &amp; D <> J &amp; D <> M &amp; E <> F &amp; E <> J &amp; E <> M &amp; F <> J &amp; F <> M &amp; J <> M holds
CompF (D,G) = (((((A '/\' B) '/\' C) '/\' E) '/\' F) '/\' J) '/\' M
proofend;

theorem Th58: :: BVFUNC14:58
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M being a_partition of Y st G = {A,B,C,D,E,F,J,M} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; A <> J &amp; A <> M &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; B <> J &amp; B <> M &amp; C <> D &amp; C <> E &amp; C <> F &amp; C <> J &amp; C <> M &amp; D <> E &amp; D <> F &amp; D <> J &amp; D <> M &amp; E <> F &amp; E <> J &amp; E <> M &amp; F <> J &amp; F <> M &amp; J <> M holds
CompF (E,G) = (((((A '/\' B) '/\' C) '/\' D) '/\' F) '/\' J) '/\' M
proofend;

theorem Th59: :: BVFUNC14:59
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M being a_partition of Y st G = {A,B,C,D,E,F,J,M} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; A <> J &amp; A <> M &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; B <> J &amp; B <> M &amp; C <> D &amp; C <> E &amp; C <> F &amp; C <> J &amp; C <> M &amp; D <> E &amp; D <> F &amp; D <> J &amp; D <> M &amp; E <> F &amp; E <> J &amp; E <> M &amp; F <> J &amp; F <> M &amp; J <> M holds
CompF (F,G) = (((((A '/\' B) '/\' C) '/\' D) '/\' E) '/\' J) '/\' M
proofend;

theorem Th60: :: BVFUNC14:60
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M being a_partition of Y st G = {A,B,C,D,E,F,J,M} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; A <> J &amp; A <> M &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; B <> J &amp; B <> M &amp; C <> D &amp; C <> E &amp; C <> F &amp; C <> J &amp; C <> M &amp; D <> E &amp; D <> F &amp; D <> J &amp; D <> M &amp; E <> F &amp; E <> J &amp; E <> M &amp; F <> J &amp; F <> M &amp; J <> M holds
CompF (J,G) = (((((A '/\' B) '/\' C) '/\' D) '/\' E) '/\' F) '/\' M
proofend;

theorem :: BVFUNC14:61
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M being a_partition of Y st G = {A,B,C,D,E,F,J,M} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; A <> J &amp; A <> M &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; B <> J &amp; B <> M &amp; C <> D &amp; C <> E &amp; C <> F &amp; C <> J &amp; C <> M &amp; D <> E &amp; D <> F &amp; D <> J &amp; D <> M &amp; E <> F &amp; E <> J &amp; E <> M &amp; F <> J &amp; F <> M &amp; J <> M holds
CompF (M,G) = (((((A '/\' B) '/\' C) '/\' D) '/\' E) '/\' F) '/\' J
proofend;

theorem Th62: :: BVFUNC14:62
for A, B, C, D, E, F, J, M being set
for h being Function
for A9, B9, C9, D9, E9, F9, J9, M9 being set st A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; A <> J &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; B <> J &amp; B <> M &amp; C <> D &amp; C <> E &amp; C <> F &amp; C <> J &amp; C <> M &amp; D <> E &amp; D <> F &amp; D <> J &amp; D <> M &amp; E <> F &amp; E <> J &amp; E <> M &amp; F <> J &amp; F <> M &amp; J <> M &amp; h = (((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (M .--> M9)) +* (A .--> A9) holds
( h . B = B9 &amp; h . C = C9 &amp; h . D = D9 &amp; h . E = E9 &amp; h . F = F9 &amp; h . J = J9 )
proofend;

theorem Th63: :: BVFUNC14:63
for A, B, C, D, E, F, J, M being set
for h being Function
for A9, B9, C9, D9, E9, F9, J9, M9 being set st h = (((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (M .--> M9)) +* (A .--> A9) holds
dom h = {A,B,C,D,E,F,J,M}
proofend;

theorem Th64: :: BVFUNC14:64
for A, B, C, D, E, F, J, M being set
for h being Function
for A9, B9, C9, D9, E9, F9, J9, M9 being set st h = (((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (M .--> M9)) +* (A .--> A9) holds
rng h = {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M)}
proofend;

theorem :: BVFUNC14:65
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M being a_partition of Y
for z, u being Element of Y st G is independent &amp; G = {A,B,C,D,E,F,J,M} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; A <> J &amp; A <> M &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; B <> J &amp; B <> M &amp; C <> D &amp; C <> E &amp; C <> F &amp; C <> J &amp; C <> M &amp; D <> E &amp; D <> F &amp; D <> J &amp; D <> M &amp; E <> F &amp; E <> J &amp; E <> M &amp; F <> J &amp; F <> M &amp; J <> M holds
(EqClass (u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M))) /\ (EqClass (z,A)) <> {}
proofend;

theorem :: BVFUNC14:66
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M being a_partition of Y
for z, u being Element of Y st G is independent &amp; G = {A,B,C,D,E,F,J,M} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; A <> J &amp; A <> M &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; B <> J &amp; B <> M &amp; C <> D &amp; C <> E &amp; C <> F &amp; C <> J &amp; C <> M &amp; D <> E &amp; D <> F &amp; D <> J &amp; D <> M &amp; E <> F &amp; E <> J &amp; E <> M &amp; F <> J &amp; F <> M &amp; J <> M &amp; 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)))
proofend;

Lm5:  for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9}
proofend;

theorem Th67: :: BVFUNC14:67
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for 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} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; A <> J &amp; A <> M &amp; A <> N &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; B <> J &amp; B <> M &amp; B <> N &amp; C <> D &amp; C <> E &amp; C <> F &amp; C <> J &amp; C <> M &amp; C <> N &amp; D <> E &amp; D <> F &amp; D <> J &amp; D <> M &amp; D <> N &amp; E <> F &amp; E <> J &amp; E <> M &amp; E <> N &amp; F <> J &amp; F <> M &amp; F <> N &amp; J <> M &amp; J <> N &amp; M <> N holds
CompF (A,G) = ((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N
proofend;

theorem Th68: :: BVFUNC14:68
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for 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} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; A <> J &amp; A <> M &amp; A <> N &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; B <> J &amp; B <> M &amp; B <> N &amp; C <> D &amp; C <> E &amp; C <> F &amp; C <> J &amp; C <> M &amp; C <> N &amp; D <> E &amp; D <> F &amp; D <> J &amp; D <> M &amp; D <> N &amp; E <> F &amp; E <> J &amp; E <> M &amp; E <> N &amp; F <> J &amp; F <> M &amp; F <> N &amp; J <> M &amp; J <> N &amp; M <> N holds
CompF (B,G) = ((((((A '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N
proofend;

theorem Th69: :: BVFUNC14:69
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for 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} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; A <> J &amp; A <> M &amp; A <> N &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; B <> J &amp; B <> M &amp; B <> N &amp; C <> D &amp; C <> E &amp; C <> F &amp; C <> J &amp; C <> M &amp; C <> N &amp; D <> E &amp; D <> F &amp; D <> J &amp; D <> M &amp; D <> N &amp; E <> F &amp; E <> J &amp; E <> M &amp; E <> N &amp; F <> J &amp; F <> M &amp; F <> N &amp; J <> M &amp; J <> N &amp; M <> N holds
CompF (C,G) = ((((((A '/\' B) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N
proofend;

theorem Th70: :: BVFUNC14:70
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for 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} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; A <> J &amp; A <> M &amp; A <> N &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; B <> J &amp; B <> M &amp; B <> N &amp; C <> D &amp; C <> E &amp; C <> F &amp; C <> J &amp; C <> M &amp; C <> N &amp; D <> E &amp; D <> F &amp; D <> J &amp; D <> M &amp; D <> N &amp; E <> F &amp; E <> J &amp; E <> M &amp; E <> N &amp; F <> J &amp; F <> M &amp; F <> N &amp; J <> M &amp; J <> N &amp; M <> N holds
CompF (D,G) = ((((((A '/\' B) '/\' C) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N
proofend;

theorem Th71: :: BVFUNC14:71
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for 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} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; A <> J &amp; A <> M &amp; A <> N &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; B <> J &amp; B <> M &amp; B <> N &amp; C <> D &amp; C <> E &amp; C <> F &amp; C <> J &amp; C <> M &amp; C <> N &amp; D <> E &amp; D <> F &amp; D <> J &amp; D <> M &amp; D <> N &amp; E <> F &amp; E <> J &amp; E <> M &amp; E <> N &amp; F <> J &amp; F <> M &amp; F <> N &amp; J <> M &amp; J <> N &amp; M <> N holds
CompF (E,G) = ((((((A '/\' B) '/\' C) '/\' D) '/\' F) '/\' J) '/\' M) '/\' N
proofend;

theorem Th72: :: BVFUNC14:72
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for 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} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; A <> J &amp; A <> M &amp; A <> N &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; B <> J &amp; B <> M &amp; B <> N &amp; C <> D &amp; C <> E &amp; C <> F &amp; C <> J &amp; C <> M &amp; C <> N &amp; D <> E &amp; D <> F &amp; D <> J &amp; D <> M &amp; D <> N &amp; E <> F &amp; E <> J &amp; E <> M &amp; E <> N &amp; F <> J &amp; F <> M &amp; F <> N &amp; J <> M &amp; J <> N &amp; M <> N holds
CompF (F,G) = ((((((A '/\' B) '/\' C) '/\' D) '/\' E) '/\' J) '/\' M) '/\' N
proofend;

theorem Th73: :: BVFUNC14:73
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for 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} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; A <> J &amp; A <> M &amp; A <> N &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; B <> J &amp; B <> M &amp; B <> N &amp; C <> D &amp; C <> E &amp; C <> F &amp; C <> J &amp; C <> M &amp; C <> N &amp; D <> E &amp; D <> F &amp; D <> J &amp; D <> M &amp; D <> N &amp; E <> F &amp; E <> J &amp; E <> M &amp; E <> N &amp; F <> J &amp; F <> M &amp; F <> N &amp; J <> M &amp; J <> N &amp; M <> N holds
CompF (J,G) = ((((((A '/\' B) '/\' C) '/\' D) '/\' E) '/\' F) '/\' M) '/\' N
proofend;

theorem Th74: :: BVFUNC14:74
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for 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} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; A <> J &amp; A <> M &amp; A <> N &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; B <> J &amp; B <> M &amp; B <> N &amp; C <> D &amp; C <> E &amp; C <> F &amp; C <> J &amp; C <> M &amp; C <> N &amp; D <> E &amp; D <> F &amp; D <> J &amp; D <> M &amp; D <> N &amp; E <> F &amp; E <> J &amp; E <> M &amp; E <> N &amp; F <> J &amp; F <> M &amp; F <> N &amp; J <> M &amp; J <> N &amp; M <> N holds
CompF (M,G) = ((((((A '/\' B) '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' N
proofend;

theorem :: BVFUNC14:75
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for 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} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; A <> J &amp; A <> M &amp; A <> N &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; B <> J &amp; B <> M &amp; B <> N &amp; C <> D &amp; C <> E &amp; C <> F &amp; C <> J &amp; C <> M &amp; C <> N &amp; D <> E &amp; D <> F &amp; D <> J &amp; D <> M &amp; D <> N &amp; E <> F &amp; E <> J &amp; E <> M &amp; E <> N &amp; F <> J &amp; F <> M &amp; F <> N &amp; J <> M &amp; J <> N &amp; M <> N holds
CompF (N,G) = ((((((A '/\' B) '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M
proofend;

theorem Th76: :: BVFUNC14:76
for A, B, C, D, E, F, J, M, N being set
for h being Function
for A9, B9, C9, D9, E9, F9, J9, M9, N9 being set st A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; A <> J &amp; A <> M &amp; A <> N &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; B <> J &amp; B <> M &amp; B <> N &amp; C <> D &amp; C <> E &amp; C <> F &amp; C <> J &amp; C <> M &amp; C <> N &amp; D <> E &amp; D <> F &amp; D <> J &amp; D <> M &amp; D <> N &amp; E <> F &amp; E <> J &amp; E <> M &amp; E <> N &amp; F <> J &amp; F <> M &amp; F <> N &amp; J <> M &amp; J <> N &amp; M <> N &amp; h = ((((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (M .--> M9)) +* (N .--> N9)) +* (A .--> A9) holds
( h . A = A9 &amp; h . B = B9 &amp; h . C = C9 &amp; h . D = D9 &amp; h . E = E9 &amp; h . F = F9 &amp; h . J = J9 &amp; h . M = M9 &amp; h . N = N9 )
proofend;

theorem Th77: :: BVFUNC14:77
for A, B, C, D, E, F, J, M, N being set
for h being Function
for A9, B9, C9, D9, E9, F9, J9, M9, N9 being set st h = ((((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (M .--> M9)) +* (N .--> N9)) +* (A .--> A9) holds
dom h = {A,B,C,D,E,F,J,M,N}
proofend;

theorem Th78: :: BVFUNC14:78
for A, B, C, D, E, F, J, M, N being set
for h being Function
for A9, B9, C9, D9, E9, F9, J9, M9, N9 being set st h = ((((((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (M .--> M9)) +* (N .--> N9)) +* (A .--> A9) holds
rng h = {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)}
proofend;

theorem :: BVFUNC14:79
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M, N being a_partition of Y
for z, u being Element of Y st G is independent &amp; G = {A,B,C,D,E,F,J,M,N} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; A <> J &amp; A <> M &amp; A <> N &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; B <> J &amp; B <> M &amp; B <> N &amp; C <> D &amp; C <> E &amp; C <> F &amp; C <> J &amp; C <> M &amp; C <> N &amp; D <> E &amp; D <> F &amp; D <> J &amp; D <> M &amp; D <> N &amp; E <> F &amp; E <> J &amp; E <> M &amp; E <> N &amp; F <> J &amp; F <> M &amp; F <> N &amp; J <> M &amp; J <> N &amp; M <> N holds
(EqClass (u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N))) /\ (EqClass (z,A)) <> {}
proofend;

theorem :: BVFUNC14:80
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M, N being a_partition of Y
for z, u being Element of Y st G is independent &amp; G = {A,B,C,D,E,F,J,M,N} &amp; A <> B &amp; A <> C &amp; A <> D &amp; A <> E &amp; A <> F &amp; A <> J &amp; A <> M &amp; A <> N &amp; B <> C &amp; B <> D &amp; B <> E &amp; B <> F &amp; B <> J &amp; B <> M &amp; B <> N &amp; C <> D &amp; C <> E &amp; C <> F &amp; C <> J &amp; C <> M &amp; C <> N &amp; D <> E &amp; D <> F &amp; D <> J &amp; D <> M &amp; D <> N &amp; E <> F &amp; E <> J &amp; E <> M &amp; E <> N &amp; F <> J &amp; F <> M &amp; F <> N &amp; J <> M &amp; J <> N &amp; M <> N &amp; 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)))
proofend;