:: 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))
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
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 & 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 & 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 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}
proof end;

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

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

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

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

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

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 & 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 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}
proof end;

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)}
proof end;

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 & 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: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 & 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;

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

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} & 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 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 & 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 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}
proof end;

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)}
proof end;

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

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} & 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 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 & 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 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}
proof end;

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)}
proof end;

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

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} & 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 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 & 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 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}
proof end;

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)}
proof end;

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 & 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: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 & 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;

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 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} & 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 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} & 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 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} & 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 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} & 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 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} & 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 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} & 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 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} & 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 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} & 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: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} & 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 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 & 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 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}
proof end;

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)}
proof end;

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 & 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: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 & 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;