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

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 TH15: :: 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 G being Subset of (PARTITIONS Y)
for A, B, C, D being a_partition of Y
for h being Function
for A', B', C', D' being set st G = {A,B,C,D} & A <> B & A <> C & A <> D & B <> C & B <> D & C <> D & h = (((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (A .--> A') holds
( h . B = B' & h . C = C' & h . D = D' )

proof end;

theorem Th19: :: BVFUNC14:19

for A, B, C, D being set
for h being Function
for A', B', C', D' being set st h = (((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (A .--> A') 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 A', B', C', D' being set st G = {A,B,C,D} & h = (((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (A .--> A') 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 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
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 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
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 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
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 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
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 A', B', C', D', E' 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 .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (A .--> A') holds
( h . A = A' & h . B = B' & h . C = C' & h . D = D' & h . E = E' )

proof end;

theorem Th30: :: BVFUNC14:30

for A, B, C, D, E being set
for h being Function
for A', B', C', D', E' being set st h = ((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (A .--> A') 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 A', B', C', D', E' being set st h = ((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (A .--> A') 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 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
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 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
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 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
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 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
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 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
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 A', B', C', D', E', F' 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 .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (A .--> A') holds
( h . A = A' & h . B = B' & h . C = C' & h . D = D' & h . E = E' & h . F = F' )

proof end;

theorem Th41: :: BVFUNC14:41

for A, B, C, D, E, F being set
for h being Function
for A', B', C', D', E', F' being set st h = (((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (A .--> A') 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 A', B', C', D', E', F' 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 .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (A .--> A') 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;

theorem TH1: :: 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 Th2: :: 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 Th3: :: 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 Th4: :: 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 Th5: :: 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 Th6: :: 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 Th8: :: BVFUNC14:52

for A, B, C, D, E, F, J being set
for h being Function
for 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' )

proof end;

theorem Th9: :: BVFUNC14:53

for A, B, C, D, E, F, J being set
for h being Function
for 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}

proof end;

theorem Th10: :: BVFUNC14:54

for A, B, C, D, E, F, J being set
for h being Function
for 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)}

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 Th13: :: 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 Th14: :: 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 Th15: :: 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 Th16: :: 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 Th17: :: 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 Th18: :: 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 Th19: :: 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 Th21: :: BVFUNC14:65

for A, B, C, D, E, F, J, M being set
for h being Function
for 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' )

proof end;

theorem Th22: :: BVFUNC14:66

for A, B, C, D, E, F, J, M being set
for h being Function
for 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}

proof end;

theorem Th23: :: BVFUNC14:67

for A, B, C, D, E, F, J, M being set
for h being Function
for 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)}

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;

Lm1: 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 Th35: :: 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 Th36: :: 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 Th37: :: 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 Th38: :: 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 Th39: :: 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 Th40: :: 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 Th41: :: 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 Th42: :: 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 Th44: :: BVFUNC14:88

for A, B, C, D, E, F, J, M, N being set
for h being Function
for 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' )

proof end;

theorem Th45: :: BVFUNC14:89

for A, B, C, D, E, F, J, M, N being set
for h being Function
for 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}

proof end;

theorem Th46: :: BVFUNC14:90

for A, B, C, D, E, F, J, M, N being set
for h being Function
for 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)}

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;