:: Predicate Calculus for Boolean Valued Functions, { VI }
:: by Shunichi Kobayashi
::
:: Received October 19, 1999
:: Copyright (c) 1999-2011 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))

proof end;

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} & A <> B holds
'/\' G = A '/\' B

proof end;

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

proof end;

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

proof end;

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

proof end;

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)}

proof end;

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} & B <> C & C <> D & D <> B holds
'/\' G = (B '/\' C) '/\' D

proof end;

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} & A <> B & C <> A holds
CompF (A,G) = B '/\' C

proof end;

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} & A <> B & B <> C holds
CompF (B,G) = C '/\' A

proof end;

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} & B <> C & C <> A holds
CompF (C,G) = A '/\' B

proof end;

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} & A <> B & A <> C & A <> D holds
CompF (A,G) = (B '/\' C) '/\' D

proof end;

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} & A <> B & B <> C & B <> D holds
CompF (B,G) = (A '/\' C) '/\' D

proof end;

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} & A <> C & B <> C & C <> D holds
CompF (C,G) = (A '/\' B) '/\' D

proof end;

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} & A <> D & B <> D & C <> D holds
CompF (D,G) = (A '/\' C) '/\' B

proof end;

theorem :: BVFUNC14:11

canceled;

theorem :: BVFUNC14:12

canceled;

theorem :: BVFUNC14:13

canceled;

theorem :: BVFUNC14:14

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

theorem :: BVFUNC14:15

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:16

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

theorem :: BVFUNC14:17

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;

theorem Th18: :: BVFUNC14:18

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 & A <> C & A <> D & B <> C & B <> D & C <> D & h = (((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (A .--> A9) holds
( h . B = B9 & h . C = C9 & h . D = D9 )

proof end;

theorem Th19: :: BVFUNC14:19

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}

proof end;

theorem Th20: :: BVFUNC14:20

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} & h = (((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (A .--> A9) holds
rng h = {(h . A),(h . B),(h . C),(h . D)}

proof end;

theorem :: BVFUNC14:21

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 & G = {A,B,C,D} & A <> B & A <> C & A <> D & B <> C & B <> D & C <> D holds
EqClass (u,((B '/\' C) '/\' D)) meets EqClass (z,A)

proof end;

theorem :: BVFUNC14:22

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 & G = {A,B,C,D} & A <> B & A <> C & A <> D & B <> C & B <> D & C <> D & EqClass (z,(C '/\' D)) = EqClass (u,(C '/\' D)) holds
EqClass (u,(CompF (A,G))) meets EqClass (z,(CompF (B,G)))

proof end;

theorem :: BVFUNC14:23

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 & G = {A,B,C} & A <> B & B <> C & C <> A & EqClass (z,C) = EqClass (u,C) holds
EqClass (u,(CompF (A,G))) meets EqClass (z,(CompF (B,G)))

proof end;

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} & A <> B & A <> C & A <> D & A <> E holds
CompF (A,G) = ((B '/\' C) '/\' D) '/\' E

proof end;

theorem Th25: :: 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} & A <> B & B <> C & B <> D & B <> E holds
CompF (B,G) = ((A '/\' C) '/\' D) '/\' E

proof end;

theorem Th26: :: BVFUNC14:26

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} & A <> C & B <> C & C <> D & C <> E holds
CompF (C,G) = ((A '/\' B) '/\' D) '/\' E

proof end;

theorem Th27: :: BVFUNC14:27

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} & A <> D & B <> D & C <> D & D <> E holds
CompF (D,G) = ((A '/\' B) '/\' C) '/\' E

proof end;

theorem :: BVFUNC14:28

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} & A <> E & B <> E & C <> E & D <> E holds
CompF (E,G) = ((A '/\' B) '/\' C) '/\' D

proof end;

theorem Th29: :: BVFUNC14:29

for A, B, C, D, E being set
for h being Function
for A9, B9, C9, D9, E9 being set st A <> B & A <> C & A <> D & A <> E & B <> C & B <> D & B <> E & C <> D & C <> E & D <> E & h = ((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (A .--> A9) holds
( h . A = A9 & h . B = B9 & h . C = C9 & h . D = D9 & h . E = E9 )

proof end;

theorem Th30: :: BVFUNC14:30

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}

proof end;

theorem Th31: :: BVFUNC14:31

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)}

proof end;

theorem :: BVFUNC14:32

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 & G = {A,B,C,D,E} & A <> B & A <> C & A <> D & A <> E & B <> C & B <> D & B <> E & C <> D & C <> E & D <> E holds
EqClass (u,(((B '/\' C) '/\' D) '/\' E)) meets EqClass (z,A)

proof end;

theorem :: BVFUNC14:33

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 & G = {A,B,C,D,E} & A <> B & A <> C & A <> D & A <> E & B <> C & B <> D & B <> E & C <> D & C <> E & D <> E & EqClass (z,((C '/\' D) '/\' E)) = EqClass (u,((C '/\' D) '/\' E)) holds
EqClass (u,(CompF (A,G))) meets EqClass (z,(CompF (B,G)))

proof end;

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} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F holds
CompF (A,G) = (((B '/\' C) '/\' D) '/\' E) '/\' F

proof end;

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} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F holds
CompF (B,G) = (((A '/\' C) '/\' D) '/\' E) '/\' F

proof end;

theorem Th36: :: 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} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F holds
CompF (C,G) = (((A '/\' B) '/\' D) '/\' E) '/\' F

proof end;

theorem Th37: :: BVFUNC14:37

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} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F holds
CompF (D,G) = (((A '/\' B) '/\' C) '/\' E) '/\' F

proof end;

theorem Th38: :: BVFUNC14:38

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} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F holds
CompF (E,G) = (((A '/\' B) '/\' C) '/\' D) '/\' F

proof end;

theorem :: BVFUNC14:39

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} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F holds
CompF (F,G) = (((A '/\' B) '/\' C) '/\' D) '/\' E

proof end;

theorem Th40: :: BVFUNC14:40

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 & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F & h = (((((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (A .--> A9) holds
( h . A = A9 & h . B = B9 & h . C = C9 & h . D = D9 & h . E = E9 & h . F = F9 )

proof end;

theorem Th41: :: BVFUNC14:41

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}

proof end;

theorem Th42: :: BVFUNC14:42

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)}

proof end;

theorem :: BVFUNC14:43

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 & G = {A,B,C,D,E,F} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F holds
EqClass (u,((((B '/\' C) '/\' D) '/\' E) '/\' F)) meets EqClass (z,A)

proof end;

theorem :: BVFUNC14:44

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 & G = {A,B,C,D,E,F} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F & EqClass (z,(((C '/\' D) '/\' E) '/\' F)) = EqClass (u,(((C '/\' D) '/\' E) '/\' F)) holds
EqClass (u,(CompF (A,G))) meets EqClass (z,(CompF (B,G)))

proof end;

begin

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} & 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
CompF (A,G) = ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J

proof end;

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} & 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
CompF (B,G) = ((((A '/\' C) '/\' D) '/\' E) '/\' F) '/\' J

proof end;

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} & 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
CompF (C,G) = ((((A '/\' B) '/\' D) '/\' E) '/\' F) '/\' J

proof end;

theorem Th48: :: 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} & 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
CompF (D,G) = ((((A '/\' B) '/\' C) '/\' E) '/\' F) '/\' J

proof end;

theorem Th49: :: BVFUNC14:49

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} & 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
CompF (E,G) = ((((A '/\' B) '/\' C) '/\' D) '/\' F) '/\' J

proof end;

theorem Th50: :: BVFUNC14:50

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} & 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
CompF (F,G) = ((((A '/\' B) '/\' C) '/\' D) '/\' E) '/\' J

proof end;

theorem :: BVFUNC14:51

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} & 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
CompF (J,G) = ((((A '/\' B) '/\' C) '/\' D) '/\' E) '/\' F

proof end;

theorem Th52: :: BVFUNC14:52

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 & 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 .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (A .--> A9) holds
( h . A = A9 & h . B = B9 & h . C = C9 & h . D = D9 & h . E = E9 & h . F = F9 & h . J = J9 )

proof end;

theorem Th53: :: BVFUNC14:53

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}

proof end;

theorem Th54: :: BVFUNC14:54

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)}

proof end;

theorem :: BVFUNC14:55

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 & 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)

proof end;

theorem :: BVFUNC14:56

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 & 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)))

proof end;

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} & 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
CompF (A,G) = (((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M

proof end;

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} & 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
CompF (B,G) = (((((A '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M

proof end;

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} & 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
CompF (C,G) = (((((A '/\' B) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M

proof end;

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} & 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
CompF (D,G) = (((((A '/\' B) '/\' C) '/\' E) '/\' F) '/\' J) '/\' M

proof end;

theorem Th61: :: 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} & 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
CompF (E,G) = (((((A '/\' B) '/\' C) '/\' D) '/\' F) '/\' J) '/\' M

proof end;

theorem Th62: :: BVFUNC14:62

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} & 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
CompF (F,G) = (((((A '/\' B) '/\' C) '/\' D) '/\' E) '/\' J) '/\' M

proof end;

theorem Th63: :: BVFUNC14:63

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} & 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
CompF (J,G) = (((((A '/\' B) '/\' C) '/\' D) '/\' E) '/\' F) '/\' M

proof end;

theorem :: BVFUNC14:64

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} & 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
CompF (M,G) = (((((A '/\' B) '/\' C) '/\' D) '/\' E) '/\' F) '/\' J

proof end;

theorem Th65: :: BVFUNC14:65

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 & A <> C & A <> D & A <> E & A <> F & A <> J & 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 .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (M .--> M9)) +* (A .--> A9) holds
( h . B = B9 & h . C = C9 & h . D = D9 & h . E = E9 & h . F = F9 & h . J = J9 )

proof end;

theorem Th66: :: BVFUNC14:66

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}

proof end;

theorem Th67: :: BVFUNC14:67

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)}

proof end;

theorem :: BVFUNC14:68

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 & 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)) <> {}

proof end;

theorem :: BVFUNC14:69

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 & 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)))

proof end;

definition

canceled;

end;

:: deftheorem BVFUNC14:def 1 :
canceled;

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}

proof end;

theorem :: BVFUNC14:70

canceled;

theorem :: BVFUNC14:71

canceled;

theorem :: BVFUNC14:72

canceled;

theorem :: BVFUNC14:73

canceled;

theorem :: BVFUNC14:74

canceled;

theorem :: BVFUNC14:75

canceled;

theorem :: BVFUNC14:76

canceled;

theorem :: BVFUNC14:77

canceled;

theorem :: BVFUNC14:78

canceled;

theorem Th79: :: 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 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

proof end;

theorem Th80: :: 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 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

proof end;

theorem Th81: :: BVFUNC14:81

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} & 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

proof end;

theorem Th82: :: BVFUNC14:82

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} & 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

proof end;

theorem Th83: :: BVFUNC14:83

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} & 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

proof end;

theorem Th84: :: BVFUNC14:84

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} & 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

proof end;

theorem Th85: :: BVFUNC14:85

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} & 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

proof end;

theorem Th86: :: BVFUNC14:86

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} & 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

proof end;

theorem :: BVFUNC14:87

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} & 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

proof end;

theorem Th88: :: BVFUNC14:88

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 & 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 .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (E .--> E9)) +* (F .--> F9)) +* (J .--> J9)) +* (M .--> M9)) +* (N .--> N9)) +* (A .--> A9) holds
( h . A = A9 & h . B = B9 & h . C = C9 & h . D = D9 & h . E = E9 & h . F = F9 & h . J = J9 & h . M = M9 & h . N = N9 )

proof end;

theorem Th89: :: BVFUNC14:89

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}

proof end;

theorem Th90: :: BVFUNC14:90

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)}

proof end;

theorem :: BVFUNC14:91

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 & 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)) <> {}

proof end;

theorem :: BVFUNC14:92

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 & 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)))

proof end;