:: Predicate Calculus for Boolean Valued Functions, { VI } :: by Shunichi Kobayashi :: :: Received October 19, 1999 :: Copyright (c) 1999-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, SUBSET_1, PARTIT1, EQREL_1, TARSKI, SETFAM_1, FUNCOP_1, RELAT_1, ZFMISC_1, FUNCT_1, FUNCT_4, BVFUNC_2; notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, SETFAM_1, EQREL_1, FUNCOP_1, PARTIT1, BVFUNC_1, BVFUNC_2, FUNCT_4; constructors ENUMSET1, SETFAM_1, FUNCT_4, BVFUNC_1, BVFUNC_2, FUNCOP_1; registrations XBOOLE_0, SUBSET_1, FUNCOP_1, FUNCT_4, EQREL_1; requirements SUBSET, BOOLE; begin :: Chap. 1 Preliminaries reserve Y for non empty set, G for Subset of PARTITIONS(Y), A,B,C,D,E,F for a_partition of Y; theorem :: BVFUNC14:1 for z being Element of Y, PA,PB being a_partition of Y holds EqClass(z,PA '/\' PB) = EqClass(z,PA) /\ EqClass(z,PB); theorem :: BVFUNC14:2 G={A,B} & A<>B implies '/\' G = A '/\' B; theorem :: BVFUNC14:3 G={B,C,D} & B<>C & C<>D & D<>B implies '/\' G = B '/\' C '/\' D; theorem :: BVFUNC14:4 G={A,B,C} & A<>B & C<>A implies CompF(A,G) = B '/\' C; theorem :: BVFUNC14:5 G={A,B,C} & A<>B & B<>C implies CompF(B,G) = C '/\' A; theorem :: BVFUNC14:6 G={A,B,C} & B<>C & C<>A implies CompF(C,G) = A '/\' B; theorem :: BVFUNC14:7 G={A,B,C,D} & A<>B & A<>C & A<>D implies CompF(A,G) = B '/\' C '/\' D; theorem :: BVFUNC14:8 G={A,B,C,D} & A<>B & B<>C & B<>D implies CompF(B,G) = A '/\' C '/\' D; theorem :: BVFUNC14:9 G={A,B,C,D} & A<>C & B<>C & C<>D implies CompF(C,G) = A '/\' B '/\' D; theorem :: BVFUNC14:10 G={A,B,C,D} & A<>D & B<>D & C<>D implies CompF(D,G) = A '/\' C '/\' B; theorem :: BVFUNC14:11 for B,C,D,b,c,d being object holds dom (B,C,D) --> (b,c,d) = {B,C,D}; theorem :: BVFUNC14:12 for f being Function, C,D,c,d being object st C<>D holds (f +* (C .--> c) +* (D .--> d)).C = c; theorem :: BVFUNC14:13 for B,C,D,b,c,d being object st B<>C & D<>B holds ((B,C,D) --> (b,c,d)).B = b; theorem :: BVFUNC14:14 for B,C,D,b,c,d being object, h being Function st h = (B,C,D) --> (b,c,d) holds rng h = {h.B,h.C,h.D}; :: from BVFUNC20 theorem :: BVFUNC14:15 for h being Function, A9,B9,C9,D9 being object 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; theorem :: BVFUNC14:16 for A,B,C,D being object,h being Function, A9,B9,C9,D9 being object st h = (B .--> B9) +* (C .--> C9) +* (D .--> D9) +* (A .--> A9) holds dom h = {A,B ,C,D}; theorem :: BVFUNC14:17 for h being Function,A9,B9,C9,D9 being object 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}; theorem :: BVFUNC14:18 for z,u being Element of Y, 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); theorem :: BVFUNC14:19 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)); theorem :: BVFUNC14:20 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)); theorem :: BVFUNC14:21 G={A,B,C,D,E} & A<>B & A<>C & A<>D & A<>E implies CompF(A,G) = B '/\' C '/\' D '/\' E; theorem :: BVFUNC14:22 G={A,B,C,D,E} & A<>B & B<>C & B<>D & B<>E implies CompF(B,G) = A '/\' C '/\' D '/\' E; theorem :: BVFUNC14:23 G={A,B,C,D,E} & A<>C & B<>C & C<>D & C<>E implies CompF(C,G) = A '/\' B '/\' D '/\' E; theorem :: BVFUNC14:24 G={A,B,C,D,E} & A<>D & B<>D & C<>D & D<>E implies CompF(D,G) = A '/\' B '/\' C '/\' E; theorem :: BVFUNC14:25 G={A,B,C,D,E} & A<>E & B<>E & C<>E & D<>E implies CompF(E,G) = A '/\' B '/\' C '/\' D; theorem :: BVFUNC14:26 for A,B,C,D,E being set, h being Function, 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; theorem :: BVFUNC14:27 for A,B,C,D,E being set, h being Function, 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}; theorem :: BVFUNC14:28 for A,B,C,D,E being set, h being Function, 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}; theorem :: BVFUNC14:29 for G being Subset of PARTITIONS(Y), A,B,C,D,E being a_partition of Y, z,u being Element of Y, 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); theorem :: BVFUNC14:30 for G being Subset of PARTITIONS(Y), A,B,C,D,E being a_partition of Y, 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)); :: moved from BVFUNC23, AG 4.01.2006 theorem :: BVFUNC14:31 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 implies CompF(A,G) = B '/\' C '/\' D '/\' E '/\' F; theorem :: BVFUNC14:32 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 implies CompF(B,G) = A '/\' C '/\' D '/\' E '/\' F; theorem :: BVFUNC14:33 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 implies CompF(C,G) = A '/\' B '/\' D '/\' E '/\' F; theorem :: BVFUNC14:34 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 implies CompF(D,G) = A '/\' B '/\' C '/\' E '/\' F; theorem :: BVFUNC14:35 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 implies CompF(E,G) = A '/\' B '/\' C '/\' D '/\' F; theorem :: BVFUNC14:36 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 implies CompF(F,G) = A '/\' B '/\' C '/\' D '/\' E; theorem :: BVFUNC14:37 for A,B,C,D,E,F being set, h being Function, 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; theorem :: BVFUNC14:38 for A,B,C,D,E,F being set, h being Function, 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}; theorem :: BVFUNC14:39 for A,B,C,D,E,F being set, h being Function, 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}; theorem :: BVFUNC14:40 for G being Subset of PARTITIONS(Y), A,B,C,D,E,F being a_partition of Y, z,u being Element of Y, h being Function st G is independent & G={A,B,C,D,E, F} & 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); theorem :: BVFUNC14:41 for G being Subset of PARTITIONS(Y), A,B,C,D,E,F being a_partition of Y, z,u being Element of Y, h being Function st G is independent & G={A,B,C,D,E, F} & 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)) ; begin :: Moved from BVFUNC24, AG 19.12.2008 reserve Y for non empty set, G for Subset of PARTITIONS(Y), A, B, C, D, E, F, J, M for a_partition of Y, x,x1,x2,x3,x4,x5,x6,x7,x8,x9 for set; theorem :: BVFUNC14:42 G={A,B,C,D,E,F,J} & A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & B <>C & B<>D & B<>E & B<>F & B<>J & C<>D & C<>E & C<>F & C<>J & D<>E & D<>F & D<> J & E<>F & E<>J & F<>J implies CompF(A,G) = B '/\' C '/\' D '/\' E '/\' F '/\' J; theorem :: BVFUNC14:43 G={A,B,C,D,E,F,J} & A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & B <>C & B<>D & B<>E & B<>F & B<>J & C<>D & C<>E & C<>F & C<>J & D<>E & D<>F & D<> J & E<>F & E<>J & F<>J implies CompF(B,G) = A '/\' C '/\' D '/\' E '/\' F '/\' J; theorem :: BVFUNC14:44 G={A,B,C,D,E,F,J} & A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & B <>C & B<>D & B<>E & B<>F & B<>J & C<>D & C<>E & C<>F & C<>J & D<>E & D<>F & D<> J & E<>F & E<>J & F<>J implies CompF(C,G) = A '/\' B '/\' D '/\' E '/\' F '/\' J; theorem :: BVFUNC14:45 G={A,B,C,D,E,F,J} & A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & B <>C & B<>D & B<>E & B<>F & B<>J & C<>D & C<>E & C<>F & C<>J & D<>E & D<>F & D<> J & E<>F & E<>J & F<>J implies CompF(D,G) = A '/\' B '/\' C '/\' E '/\' F '/\' J; theorem :: BVFUNC14:46 G={A,B,C,D,E,F,J} & A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & B <>C & B<>D & B<>E & B<>F & B<>J & C<>D & C<>E & C<>F & C<>J & D<>E & D<>F & D<> J & E<>F & E<>J & F<>J implies CompF(E,G) = A '/\' B '/\' C '/\' D '/\' F '/\' J; theorem :: BVFUNC14:47 G={A,B,C,D,E,F,J} & A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & B <>C & B<>D & B<>E & B<>F & B<>J & C<>D & C<>E & C<>F & C<>J & D<>E & D<>F & D<> J & E<>F & E<>J & F<>J implies CompF(F,G) = A '/\' B '/\' C '/\' D '/\' E '/\' J; theorem :: BVFUNC14:48 G={A,B,C,D,E,F,J} & A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & B<>C & B <>D & B<>E & B<>F & B<>J & C<>D & C<>E & C<>F & C<>J & D<>E & D<>F & D<>J & E<> F & E<>J & F<>J implies CompF(J,G) = A '/\' B '/\' C '/\' D '/\' E '/\' F; theorem :: BVFUNC14:49 for A,B,C,D,E,F,J being set, h being Function, 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; theorem :: BVFUNC14:50 for A,B,C,D,E,F,J being set, h being Function, 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}; theorem :: BVFUNC14:51 for A,B,C,D,E,F,J being set, h being Function, 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}; theorem :: BVFUNC14:52 for G being Subset of PARTITIONS(Y), A,B,C,D,E,F,J being a_partition of Y, z,u being Element of Y st G is independent & G={A,B,C,D,E,F,J} & A<>B & A <>C & A<>D & A<>E & A<>F & A<>J & B<>C & B<>D & B<>E & B<>F & B<>J & C<>D & C<> E & C<>F & C<>J & D<>E & D<>F & D<>J & E<>F & E<>J & F<>J holds EqClass(u,B '/\' C '/\' D '/\' E '/\' F '/\' J) meets EqClass(z,A); theorem :: BVFUNC14:53 for G being Subset of PARTITIONS(Y), A,B,C,D,E,F,J being a_partition of Y, z,u being Element of Y st G is independent & G={A,B,C,D,E,F,J} & A<>B & A <>C & A<>D & A<>E & A<>F & A<>J & B<>C & B<>D & B<>E & B<>F & B<>J & C<>D & C<> E & C<>F & C<>J & D<>E & D<>F & D<>J & E<>F & E<>J & F<>J & EqClass(z,C '/\' D '/\' E '/\' F '/\' J)= EqClass(u,C '/\' D '/\' E '/\' F '/\' J) holds EqClass(u ,CompF(A,G)) meets EqClass(z,CompF(B,G)); theorem :: BVFUNC14:54 G={A,B,C,D,E,F,J,M} & A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M & B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & C<>D & C<>E & C<>F & C<>J & C <>M & D<>E & D<>F & D<>J & D<>M & E<>F & E<>J & E<>M & F<>J & F<>M & J<>M implies CompF(A,G) = B '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M; theorem :: BVFUNC14:55 G={A,B,C,D,E,F,J,M} & A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M & B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & C<>D & C<>E & C<>F & C<>J & C <>M & D<>E & D<>F & D<>J & D<>M & E<>F & E<>J & E<>M & F<>J & F<>M & J<>M implies CompF(B,G) = A '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M; theorem :: BVFUNC14:56 G={A,B,C,D,E,F,J,M} & A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M & B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & C<>D & C<>E & C<>F & C<>J & C <>M & D<>E & D<>F & D<>J & D<>M & E<>F & E<>J & E<>M & F<>J & F<>M & J<>M implies CompF(C,G) = A '/\' B '/\' D '/\' E '/\' F '/\' J '/\' M; theorem :: BVFUNC14:57 G={A,B,C,D,E,F,J,M} & A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M & B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & C<>D & C<>E & C<>F & C<>J & C <>M & D<>E & D<>F & D<>J & D<>M & E<>F & E<>J & E<>M & F<>J & F<>M & J<>M implies CompF(D,G) = A '/\' B '/\' C '/\' E '/\' F '/\' J '/\' M; theorem :: BVFUNC14:58 G={A,B,C,D,E,F,J,M} & A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M & B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & C<>D & C<>E & C<>F & C<>J & C <>M & D<>E & D<>F & D<>J & D<>M & E<>F & E<>J & E<>M & F<>J & F<>M & J<>M implies CompF(E,G) = A '/\' B '/\' C '/\' D '/\' F '/\' J '/\' M; theorem :: BVFUNC14:59 G={A,B,C,D,E,F,J,M} & A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M & B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & C<>D & C<>E & C<>F & C<>J & C <>M & D<>E & D<>F & D<>J & D<>M & E<>F & E<>J & E<>M & F<>J & F<>M & J<>M implies CompF(F,G) = A '/\' B '/\' C '/\' D '/\' E '/\' J '/\' M; theorem :: BVFUNC14:60 G={A,B,C,D,E,F,J,M} & A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M & B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & C<>D & C<>E & C<>F & C<>J & C <>M & D<>E & D<>F & D<>J & D<>M & E<>F & E<>J & E<>M & F<>J & F<>M & J<>M implies CompF(J,G) = A '/\' B '/\' C '/\' D '/\' E '/\' F '/\' M; theorem :: BVFUNC14:61 G={A,B,C,D,E,F,J,M} & A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M & B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & C<>D & C<>E & C<>F & C<>J & C<>M & D <>E & D<>F & D<>J & D<>M & E<>F & E<>J & E<>M & F<>J & F<>M & J<>M implies CompF(M,G) = A '/\' B '/\' C '/\' D '/\' E '/\' F '/\' J; theorem :: BVFUNC14:62 for A,B,C,D,E,F,J,M being set, h being Function, 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; theorem :: BVFUNC14:63 for A,B,C,D,E,F,J,M being set, h being Function, 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}; theorem :: BVFUNC14:64 for A,B,C,D,E,F,J,M being set, h being Function, 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}; theorem :: BVFUNC14:65 for G being Subset of PARTITIONS(Y), A,B,C,D,E,F,J,M being a_partition of Y, z,u being Element of Y st G is independent & G={A,B,C,D,E,F,J,M} & A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M & B<>C & B<>D & B<>E & B<>F & B<>J & B <>M & C<>D & C<>E & C<>F & C<>J & C<>M & D<>E & D<>F & D<>J & D<>M & E<>F & E<> J & E<>M & F<>J & F<>M & J<>M holds EqClass(u,B '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M) /\ EqClass(z,A) <> {}; theorem :: BVFUNC14:66 for G being Subset of PARTITIONS(Y), A,B,C,D,E,F,J,M being a_partition of Y, z,u being Element of Y st G is independent & G={A,B,C,D,E,F,J,M} & A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M & B<>C & B<>D & B<>E & B<>F & B<>J & B <>M & C<>D & C<>E & C<>F & C<>J & C<>M & D<>E & D<>F & D<>J & D<>M & E<>F & E<> J & E<>M & F<>J & F<>M & J<>M & EqClass(z,C '/\' D '/\' E '/\' F '/\' J '/\' M) = EqClass(u,C '/\' D '/\' E '/\' F '/\' J '/\' M) holds EqClass(u,CompF(A,G)) meets EqClass(z,CompF(B,G)); theorem :: BVFUNC14:67 for G being Subset of PARTITIONS(Y), A,B,C,D,E,F,J,M,N being a_partition of Y st G={A,B,C,D,E,F,J,M,N} & A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M & A<>N & B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & B<>N & C<>D & C <>E & C<>F & C<>J & C<>M & C<>N & D<>E & D<>F & D<>J & D<>M & D<>N & E<>F & E<> J & E<>M & E<>N & F<>J & F<>M & F<>N & J<>M & J<>N & M<>N holds CompF(A,G) = B '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M '/\' N; theorem :: BVFUNC14:68 for G being Subset of PARTITIONS(Y), A,B,C,D,E,F,J,M,N being a_partition of Y st G={A,B,C,D,E,F,J,M,N} & A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M & A<>N & B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & B<>N & C<>D & C <>E & C<>F & C<>J & C<>M & C<>N & D<>E & D<>F & D<>J & D<>M & D<>N & E<>F & E<> J & E<>M & E<>N & F<>J & F<>M & F<>N & J<>M & J<>N & M<>N holds CompF(B,G) = A '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M '/\' N; theorem :: BVFUNC14:69 for G being Subset of PARTITIONS(Y), A,B,C,D,E,F,J,M,N being a_partition of Y st G={A,B,C,D,E,F,J,M,N} & A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M & A<>N & B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & B<>N & C<>D & C <>E & C<>F & C<>J & C<>M & C<>N & D<>E & D<>F & D<>J & D<>M & D<>N & E<>F & E<> J & E<>M & E<>N & F<>J & F<>M & F<>N & J<>M & J<>N & M<>N holds CompF(C,G) = A '/\' B '/\' D '/\' E '/\' F '/\' J '/\' M '/\' N; theorem :: BVFUNC14:70 for G being Subset of PARTITIONS(Y), A,B,C,D,E,F,J,M,N being a_partition of Y st G={A,B,C,D,E,F,J,M,N} & A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M & A<>N & B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & B<>N & C<>D & C <>E & C<>F & C<>J & C<>M & C<>N & D<>E & D<>F & D<>J & D<>M & D<>N & E<>F & E<> J & E<>M & E<>N & F<>J & F<>M & F<>N & J<>M & J<>N & M<>N holds CompF(D,G) = A '/\' B '/\' C '/\' E '/\' F '/\' J '/\' M '/\' N; theorem :: BVFUNC14:71 for G being Subset of PARTITIONS(Y), A,B,C,D,E,F,J,M,N being a_partition of Y st G={A,B,C,D,E,F,J,M,N} & A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M & A<>N & B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & B<>N & C<>D & C <>E & C<>F & C<>J & C<>M & C<>N & D<>E & D<>F & D<>J & D<>M & D<>N & E<>F & E<> J & E<>M & E<>N & F<>J & F<>M & F<>N & J<>M & J<>N & M<>N holds CompF(E,G) = A '/\' B '/\' C '/\' D '/\' F '/\' J '/\' M '/\' N; theorem :: BVFUNC14:72 for G being Subset of PARTITIONS(Y), A,B,C,D,E,F,J,M,N being a_partition of Y st G={A,B,C,D,E,F,J,M,N} & A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M & A<>N & B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & B<>N & C<>D & C <>E & C<>F & C<>J & C<>M & C<>N & D<>E & D<>F & D<>J & D<>M & D<>N & E<>F & E<> J & E<>M & E<>N & F<>J & F<>M & F<>N & J<>M & J<>N & M<>N holds CompF(F,G) = A '/\' B '/\' C '/\' D '/\' E '/\' J '/\' M '/\' N; theorem :: BVFUNC14:73 for G being Subset of PARTITIONS(Y), A,B,C,D,E,F,J,M,N being a_partition of Y st G={A,B,C,D,E,F,J,M,N} & A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M & A<>N & B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & B<>N & C<>D & C <>E & C<>F & C<>J & C<>M & C<>N & D<>E & D<>F & D<>J & D<>M & D<>N & E<>F & E<> J & E<>M & E<>N & F<>J & F<>M & F<>N & J<>M & J<>N & M<>N holds CompF(J,G) = A '/\' B '/\' C '/\' D '/\' E '/\' F '/\' M '/\' N; theorem :: BVFUNC14:74 for G being Subset of PARTITIONS(Y), A,B,C,D,E,F,J,M,N being a_partition of Y st G={A,B,C,D,E,F,J,M,N} & A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M & A<>N & B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & B<>N & C<>D & C <>E & C<>F & C<>J & C<>M & C<>N & D<>E & D<>F & D<>J & D<>M & D<>N & E<>F & E<> J & E<>M & E<>N & F<>J & F<>M & F<>N & J<>M & J<>N & M<>N holds CompF(M,G) = A '/\' B '/\' C '/\' D '/\' E '/\' F '/\' J '/\' N; theorem :: BVFUNC14:75 for G being Subset of PARTITIONS(Y), A,B,C,D,E,F,J,M,N being a_partition of Y st G={A,B,C,D,E,F,J,M,N} & A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M & A<>N & B<>C & B<>D & B<>E & B<>F & B<>J & B<>M & B<>N & C<>D & C <>E & C<>F & C<>J & C<>M & C<>N & D<>E & D<>F & D<>J & D<>M & D<>N & E<>F & E<> J & E<>M & E<>N & F<>J & F<>M & F<>N & J<>M & J<>N & M<>N holds CompF(N,G) = A '/\' B '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M; theorem :: BVFUNC14:76 for A,B,C,D,E,F,J,M,N being set, h being Function, 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; theorem :: BVFUNC14:77 for A,B,C,D,E,F,J,M,N being set, h being Function, 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}; theorem :: BVFUNC14:78 for A,B,C,D,E,F,J,M,N being set, h being Function, 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}; theorem :: BVFUNC14:79 for G being Subset of PARTITIONS(Y), A,B,C,D,E,F,J,M,N being a_partition of Y, z,u being Element of Y st G is independent & G={A,B,C,D,E,F,J ,M,N} & A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M & A<>N & B<>C & B<>D & B <>E & B<>F & B<>J & B<>M & B<>N & C<>D & C<>E & C<>F & C<>J & C<>M & C<>N & D<> E & D<>F & D<>J & D<>M & D<>N & E<>F & E<>J & E<>M & E<>N & F<>J & F<>M & F<>N & J<>M & J<>N & M<>N holds EqClass(u,B '/\' C '/\' D '/\' E '/\' F '/\' J '/\' M '/\' N) /\ EqClass(z,A) <> {}; theorem :: BVFUNC14:80 for G being Subset of PARTITIONS(Y), A,B,C,D,E,F,J,M,N being a_partition of Y, z,u being Element of Y st G is independent & G={A,B,C,D,E,F,J ,M,N} & A<>B & A<>C & A<>D & A<>E & A<>F & A<>J & A<>M & A<>N & B<>C & B<>D & B <>E & B<>F & B<>J & B<>M & B<>N & C<>D & C<>E & C<>F & C<>J & C<>M & C<>N & D<> E & D<>F & D<>J & D<>M & D<>N & E<>F & E<>J & E<>M & E<>N & F<>J & F<>M & F<>N & J<>M & J<>N & M<>N & EqClass(z,C '/\' D '/\' E '/\' F '/\' J '/\' M '/\' N)= EqClass(u,C '/\' D '/\' E '/\' F '/\' J '/\' M '/\' N) holds EqClass(u,CompF(A, G)) meets EqClass(z,CompF(B,G));