### The Mizar article:

### Semilattice Operations on Finite Subsets

**by****Andrzej Trybulec**

- Received September 18, 1989
Copyright (c) 1989 Association of Mizar Users

- MML identifier: SETWISEO
- [ MML identifier index ]

environ vocabulary BOOLE, FUNCT_1, RELAT_1, FINSUB_1, FINSET_1, BINOP_1, FUNCOP_1, TARSKI, SETWISEO; notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, RELAT_1, FUNCT_1, FINSUB_1, FINSET_1, FUNCT_2, BINOP_1, FUNCOP_1; constructors TARSKI, ENUMSET1, FINSUB_1, FINSET_1, BINOP_1, FUNCOP_1, XBOOLE_0; clusters FINSET_1, FINSUB_1, RELSET_1, XBOOLE_0, ZFMISC_1; requirements BOOLE, SUBSET; definitions BINOP_1, TARSKI; theorems FINSUB_1, ZFMISC_1, SUBSET_1, BINOP_1, TARSKI, FUNCT_1, FUNCT_2, FUNCOP_1, FINSET_1, ENUMSET1, RELAT_1, XBOOLE_0, XBOOLE_1; schemes FINSET_1, FUNCT_2, BINOP_1, XBOOLE_0; begin :: A u x i l i a r y T h e o r e m s reserve x,y,z,X,Y for set; canceled 2; theorem Th3: {x} c= {x,y,z} proof {x,y,z} = {x} \/ {y,z} by ENUMSET1:42; hence thesis by XBOOLE_1:7; end ; theorem Th4: {x,y} c= {x,y,z} proof {x,y,z} = {x,y} \/ {z} by ENUMSET1:43; hence thesis by XBOOLE_1:7; end ; theorem Th5: X c= Y \/ {x} implies x in X or X c= Y proof assume that A1: X c= Y \/ {x} and A2: not x in X; A3: X misses {x} by A2,ZFMISC_1:56; X = X /\ (Y \/ {x}) by A1,XBOOLE_1:28 .= X /\ Y \/ X /\ {x} by XBOOLE_1:23 .= X /\ Y \/ {} by A3,XBOOLE_0:def 7 .= X /\ Y; hence X c= Y by XBOOLE_1:17; end; theorem Th6: x in X \/ {y} iff x in X or x = y proof (x in X \/ {y} iff x in X or x in {y}) & (x in {y} iff x = y) by TARSKI:def 1,XBOOLE_0:def 2; hence thesis; end; canceled; theorem Th8: X \/ {x} c= Y iff x in Y & X c= Y proof A1: X \/ {x} c= Y implies X c= Y & {x} c= Y by XBOOLE_1:11; X c= Y & {x} c= Y implies X \/ {x} c= Y by XBOOLE_1:8; hence thesis by A1,ZFMISC_1:37; end; canceled 2; theorem Th11: for X,Y for f being Function holds f.:(Y \ f"X) = f.:Y \ X proof let X,Y; let f be Function; now let x; thus x in f.:(Y \ f"X) implies x in f.:Y \ X proof assume x in f.:(Y \ f"X); then consider z such that A1: z in dom f and A2: z in Y \ f"X and A3: f.z = x by FUNCT_1:def 12; not z in f"X by A2,XBOOLE_0:def 4; then A4: not x in X by A1,A3,FUNCT_1:def 13; z in Y by A2,XBOOLE_0:def 4; then f.z in f.:Y by A1,FUNCT_1:def 12; hence x in f.:Y \ X by A3,A4,XBOOLE_0:def 4; end; assume A5: x in f.:Y \ X; then x in f.:Y by XBOOLE_0:def 4; then consider z such that A6: z in dom f and A7: z in Y and A8: f.z = x by FUNCT_1:def 12; not x in X by A5,XBOOLE_0:def 4; then not z in f"X by A8,FUNCT_1:def 13; then z in Y \ f"X by A7,XBOOLE_0:def 4; hence x in f.:(Y \ f"X) by A6,A8,FUNCT_1:def 12; end; hence thesis by TARSKI:2; end; reserve X,Y for non empty set, f for Function of X,Y; theorem Th12: for x being Element of X holds x in f"{f.x} proof let x be Element of X; f.x in {f.x} by TARSKI:def 1; hence x in f"{f.x} by FUNCT_2:46; end; theorem Th13: for x being Element of X holds f.:{x} = {f.x} proof let x be Element of X; for y holds y in f.:{x} iff y = f.x proof let y; thus y in f.:{x} implies y = f.x proof assume y in f.:{x}; then ex z st z in dom f & z in {x} & f.z = y by FUNCT_1:def 12; hence y = f.x by TARSKI:def 1; end; x in {x} by TARSKI:def 1; hence thesis by FUNCT_2:43; end; hence f.:{x} = {f.x} by TARSKI:def 1; end; scheme SubsetEx { A() -> non empty set, P[set] } : ex B being Subset of A() st for x being Element of A() holds x in B iff P[x] proof defpred X[set] means P[$1]; consider B being set such that A1: for x being set holds x in B iff x in A() & X[x] from Separation; for x being set holds x in B implies x in A() by A1; then reconsider B as Subset of A() by TARSKI:def 3; take B; let x be Element of A(); thus x in B iff P[x] by A1; end; :: Theorems related to Fin ... theorem Th14: for B being Element of Fin X for x st x in B holds x is Element of X proof let B be Element of Fin X; let x such that A1: x in B; B c= X by FINSUB_1:def 5; hence x is Element of X by A1; end; theorem for A being (Element of Fin X), B being set for f being Function of X,Y st for x being Element of X holds x in A implies f.x in B holds f.:A c= B proof let A be (Element of Fin X), B be set; let f be Function of X,Y such that A1: for x being Element of X holds x in A implies f.x in B; let x be set; assume x in f.:A; then consider y being set such that y in dom f and A2:y in A and A3:x = f.y by FUNCT_1:def 12; reconsider y as Element of X by A2,Th14; x = f.y by A3; hence x in B by A1,A2; end; theorem Th16: for X being set for B being Element of Fin X for A being set st A c= B holds A is Element of Fin X proof let X be set, B be Element of Fin X; let A be set such that A1: A c= B; B c= X by FINSUB_1:def 5; then A2: A c= X by A1,XBOOLE_1:1; A is finite by A1,FINSET_1:13; hence A is Element of Fin X by A2,FINSUB_1:def 5; end; Lm1: for A being Element of Fin X holds f.: A is Element of Fin Y by FINSUB_1:def 5; canceled; theorem Th18: for B being Element of Fin X st B <> {} ex x being Element of X st x in B proof let B be Element of Fin X; assume A1: B <> {}; consider x being Element of B; reconsider x as Element of X by A1,Th14; take x; thus x in B by A1; end; theorem Th19: for A being Element of Fin X holds f.:A = {} implies A = {} proof let A be Element of Fin X; assume A1: f.:A = {}; assume A <> {}; then consider x being Element of X such that A2: x in A by Th18; f.x in f.:A by A2,FUNCT_2:43; hence contradiction by A1; end; definition let X be set; cluster empty Element of Fin X; existence proof {} is Element of Fin X by FINSUB_1:18; hence thesis; end; end; definition let X be set; func {}.X -> empty Element of Fin X equals {}; coherence by FINSUB_1:18; correctness; end; scheme FinSubFuncEx{ A()->non empty set , B()->(Element of Fin A()), P[set,set] } : ex f being Function of A(), Fin A() st for b,a being Element of A() holds a in f.b iff a in B() & P[a,b] proof defpred X[set,Element of Fin A()] means for a being Element of A() holds a in $2 iff a in B() & P[a,$1]; A1: now let x be Element of A(); defpred X[set] means $1 in B() & P[$1,x]; consider y being Subset of A() such that A2: for a being Element of A() holds a in y iff X[a] from SubsetEx; reconsider B = B() as Subset of A() by FINSUB_1:def 5; for x being Element of A() holds x in y implies x in B by A2; then y c= B() by SUBSET_1:7; then y is finite by FINSET_1:13; then reconsider y as Element of Fin A() by FINSUB_1:def 5; take y' = y; thus X[x,y'] by A2; end; thus ex f being Function of A(), Fin A() st for x being Element of A() holds X[x,f.x] from FuncExD(A1); end; :: theorems related to BinOp of ... definition let X be non empty set, F be BinOp of X; attr F is having_a_unity means :Def2: ex x being Element of X st x is_a_unity_wrt F; synonym F has_a_unity; end; canceled 2; theorem Th22: for X being non empty set, F being BinOp of X holds F has_a_unity iff the_unity_wrt F is_a_unity_wrt F proof let X be non empty set, F be BinOp of X; thus F has_a_unity implies the_unity_wrt F is_a_unity_wrt F proof assume F has_a_unity; then ex x being Element of X st x is_a_unity_wrt F by Def2; hence the_unity_wrt F is_a_unity_wrt F by BINOP_1:def 8; end; thus thesis by Def2; end; theorem Th23: for X being non empty set, F being BinOp of X st F has_a_unity for x being Element of X holds F.(the_unity_wrt F, x) = x & F.(x, the_unity_wrt F) = x proof let X be non empty set, F be BinOp of X such that A1: F has_a_unity; let x be Element of X; the_unity_wrt F is_a_unity_wrt F by A1,Th22; hence F.(the_unity_wrt F, x) = x & F.(x, the_unity_wrt F) = x by BINOP_1:11 ; end; :: M a i n p a r t definition let X be non empty set; cluster non empty Element of Fin X; existence proof consider x being Element of X; {x} is Subset of X by SUBSET_1:63; then {x} is Element of Fin X by FINSUB_1:def 5; hence thesis; end; end; definition let X be non empty set, x be Element of X; redefine func {x} -> Element of Fin X; coherence proof {x} is Subset of X by SUBSET_1:63; hence {x} is Element of Fin X by FINSUB_1:def 5; end; let y be Element of X; func {x,y} -> Element of Fin X; coherence proof {x,y} is Subset of X by SUBSET_1:56; hence {x,y} is Element of Fin X by FINSUB_1:def 5; end; let z be Element of X; func {x,y,z} -> Element of Fin X; coherence proof {x,y,z} is Subset of X by SUBSET_1:57; hence {x,y,z} is Element of Fin X by FINSUB_1:def 5; end; end; definition let X be set; let A,B be Element of Fin X; redefine func A \/ B -> Element of Fin X; coherence by FINSUB_1:10; end; definition let X be set; let A,B be Element of Fin X; redefine func A \ B -> Element of Fin X; coherence by FINSUB_1:10; end; scheme FinSubInd1{ X() -> non empty set, P[set] } : for B being Element of Fin X() holds P[B] provided A1: P[{}.X()] and A2: for B' being (Element of Fin X()), b being Element of X() holds P[B'] & not b in B' implies P[B' \/ {b}] proof let B be Element of Fin X(); defpred X[set] means ex B' being Element of Fin X() st B' = $1 & P[B']; A3: B is finite; A4: X[{}] by A1; A5: for x,A being set st x in B & A c= B & X[A] holds X[A \/ {x}] proof let x,A be set such that A6: x in B and A7: A c= B and A8: ex B' being Element of Fin X() st B' = A & P[B']; reconsider A' = A as Element of Fin X() by A7,Th16; reconsider x' = x as Element of X() by A6,Th14; take A' \/ {x'}; thus A' \/ {x'} = A \/ {x}; not x' in A or A \/ {x'} = A by ZFMISC_1:46; hence P[A' \/ {x'}] by A2,A8; end; X[B] from Finite(A3,A4,A5); hence thesis; end; scheme FinSubInd2{ X() -> non empty set, P[Element of Fin X()] } : for B being Element of Fin X() st B <> {} holds P[B] provided A1: for x being Element of X() holds P[{x}] and A2: for B1,B2 being Element of Fin X() st B1 <> {} & B2 <> {} holds P[B1] & P[B2] implies P[B1 \/ B2] proof let B be Element of Fin X(); A3: B is finite; defpred X[set] means $1 <> {} implies ex B' being Element of Fin X() st B' = $1 & P[B']; A4: X[{}]; A5: for x,A being set st x in B & A c= B & X[A] holds X[A \/ {x}] proof let x,A be set such that A6: x in B and A7: A c= B and A8: A <> {} implies ex B' being Element of Fin X() st B' = A & P[B'] and A \/ {x} <> {}; reconsider A' = A as Element of Fin X() by A7,Th16; reconsider x' = x as Element of X() by A6,Th14; take A' \/ {x'}; thus A' \/ {x'} =A \/ {x}; A9: P[{x'}] by A1; now per cases; suppose A = {}; hence P[A' \/ {x'}] by A1; suppose A <> {}; hence P[A' \/ {x'}] by A2,A8,A9; end; hence P[A' \/ {x'}]; end; X[B] from Finite(A3,A4,A5); hence thesis; end; scheme FinSubInd3{ X() -> non empty set, P[set] } : for B being Element of Fin X() holds P[B] provided A1: P[{}.X()] and A2: for B' being (Element of Fin X()), b being Element of X() holds P[B'] implies P[B' \/ {b}] proof defpred X[set] means P[$1]; A3: X[{}.X()] by A1; A4: for B' being (Element of Fin X()), b being Element of X() holds X[B'] & not b in B' implies X[B' \/ {b}] by A2; thus for B being Element of Fin X() holds X[B] from FinSubInd1(A3,A4); end; definition let X, Y be non empty set; let F be BinOp of Y; let B be Element of Fin X; let f be Function of X,Y; assume that A1: B <> {} or F has_a_unity and A2: F is commutative and A3: F is associative; func F $$ (B,f) -> Element of Y means :Def3: ex G being Function of Fin X, Y st it = G.B & (for e being Element of Y st e is_a_unity_wrt F holds G.{} = e) & (for x being Element of X holds G.{x} = f.x) & for B' being Element of Fin X st B' c= B & B' <> {} for x being Element of X st x in B \ B' holds G.(B' \/ {x}) = F.(G.B',f.x); existence proof defpred X[set] means ex G being Function of Fin X, Y st (for e being Element of Y st e is_a_unity_wrt F holds G.{} = e) & (for x being Element of X holds G.{x} = f.x) & for B' being Element of Fin X st B' c= $1 & B' <> {} for x being Element of X st x in $1 \ B' holds G.(B' \/ {x}) = F.(G.B', f.x); A4: X[{}.X] proof consider e being Element of Y such that A5: (ex e being Element of Y st e is_a_unity_wrt F) implies e = the_unity_wrt F; defpred X[set,set] means (for x' being Element of X st $1 = {x'} holds $2 = f.x') & (not (ex x' being Element of X st $1 = {x'}) implies $2 = e); A6: now let x be Element of Fin X; thus ex y being Element of Y st X[x,y] proof A7: now given x' being Element of X such that A8: x = {x'}; take y = f.x'; thus for x' being Element of X st x = {x'} holds y = f.x' by A8,ZFMISC_1:6; thus not (ex x' being Element of X st x = {x'}) implies y = e by A8; end; now assume A9: not ex x' being Element of X st x = {x'}; take y = e; thus (for x' being Element of X st x = {x'} holds y = f.x') & (not (ex x' being Element of X st x = {x'}) implies y = e) by A9; end; hence thesis by A7; end; end; consider G' being Function of Fin X, Y such that A10: for B' being Element of Fin X holds X[B',G'.B'] from FuncExD(A6); take G = G'; thus for e being Element of Y st e is_a_unity_wrt F holds G.{} = e proof let e' be Element of Y such that A11: e' is_a_unity_wrt F; reconsider E = {} as Element of Fin X by FINSUB_1:18; not ex x' being Element of X st E = {x'}; hence G.{} = e by A10 .= e' by A5,A11,BINOP_1:def 8; end; thus for x being Element of X holds G.{x} = f.x by A10; thus for B' being Element of Fin X st B' c= {}.X & B' <> {} for x being Element of X st x in {}.X \ B' holds G.(B' \/ {x}) = F.(G.B', f.x); end; A12: for B' being Element of Fin X, b being Element of X holds X[B'] & not b in B' implies X[B' \/ {b}] proof let B be (Element of Fin X), x be Element of X; given G being Function of Fin X, Y such that A13: for e being Element of Y st e is_a_unity_wrt F holds G.{} = e and A14: for x being Element of X holds G.{x} = f.x and A15: for B' being Element of Fin X st B' c= B & B' <> {} for x being Element of X st x in B \ B' holds G.(B' \/ {x}) = F.(G.B', f.x); assume A16: not x in B; thus ex G being Function of Fin X, Y st (for e being Element of Y st e is_a_unity_wrt F holds G.{} = e) & (for x being Element of X holds G.{x} = f.x) & for B' being Element of Fin X st B' c= B \/ {x} & B' <> {} for x' being Element of X st x' in (B \/ {x}) \ B' holds G.(B' \/ {x'}) = F.(G.B', f.x') proof defpred X[set,set] means (for C being Element of Fin X st C <> {} & C c= B & $1 = C \/ {x} holds $2 = F.(G.C, f.x)) & ((not ex C being Element of Fin X st C <> {} & C c= B & $1 = C \/ {x}) implies $2 = G.$1); A17: now let B' be Element of Fin X; thus ex y being Element of Y st X[B',y] proof A18: now given C being Element of Fin X such that A19: C <> {} & C c= B & B' = C \/ {x}; take y = F.(G.C, f.x); for C being Element of Fin X st C <> {} & C c= B & B' = C \/ {x} holds y = F.(G.C, f.x) proof let C1 be Element of Fin X such that A20: C1 <> {} & C1 c= B & B' = C1 \/ {x}; now A21: not x in C & not x in C1 by A16,A19,A20; C c= B' & C1 c= B' by A19,A20,XBOOLE_1:7; then A22: C c= B' \ {x} & C1 c= B' \ {x} by A21,ZFMISC_1:40; A23: B' \ {x} = C \ {x} & B' \{x} = C1 \ {x} by A19,A20, XBOOLE_1:40; C \ {x} c= C & C1 \{x} c= C1 by XBOOLE_1:36; then B' \ {x} = C & B' \ {x} = C1 by A22,A23,XBOOLE_0:def 10; hence y = F.(G.C1, f.x); end; hence y = F.(G.C1, f.x); end; hence thesis by A19; end; now assume A24: not ex C being Element of Fin X st C <> {} & C c= B & B' = C \/ {x}; take y = G.B'; thus for C being Element of Fin X st C <> {} & C c= B & B' = C \/ {x} holds y = F.(G.C, f.x) by A24; thus (not ex C being Element of Fin X st C <> {} & C c= B & B' = C \/ {x}) implies y = G.B'; end; hence thesis by A18; end; end; consider H being Function of Fin X, Y such that A25: for B' being Element of Fin X holds X[B',H.B'] from FuncExD(A17); take J = H; thus for e being Element of Y st e is_a_unity_wrt F holds J.{} = e proof reconsider E = {} as Element of Fin X by FINSUB_1:18; not ex C being Element of Fin X st C <> {} & C c= B & E = C \/ {x } ; then J.E = G.E by A25; hence thesis by A13; end; thus for x being Element of X holds J.{x} = f.x proof let x' be Element of X; now given C being Element of Fin X such that A26: C <> {} and A27: C c= B and A28: {x'} = C \/ {x}; C c= {x'} & {x} c= {x'} by A28,XBOOLE_1:7; then C = {x'} & x = x' by A26,ZFMISC_1:24,39; then x in C by TARSKI:def 1; hence contradiction by A16,A27; end; hence J.{x'} = G.{x'} by A25 .= f.x' by A14; end; let B' be Element of Fin X such that A29: B' c= B \/ {x} and A30: B' <> {}; now given C being Element of Fin X such that A31: C <> {} and A32: C c= B and A33: {x} = C \/ {x}; C c= {x} by A33,XBOOLE_1:7; then C = {x} by A31,ZFMISC_1:39; then x in C by TARSKI:def 1; hence contradiction by A16,A32; end; then A34: J.{x} = G.{x} by A25; let x' be Element of X; assume x' in (B \/ {x}) \ B'; then A35: x' in B \/ {x} & not x' in B' by XBOOLE_0:def 4; now per cases; suppose A36: x in B'; then A37: x' in B by A35,Th6; then A38: {x'} c= B by ZFMISC_1:37; now per cases; suppose A39: B' = {x}; hence J.(B' \/ {x'}) = F.(G.{x'}, f.x) by A25,A38 .= F.(f.x', f.x) by A14 .= F.(f.x, f.x') by A2,BINOP_1:def 2 .= F.(J.B', f.x') by A14,A34,A39; suppose A40: B' <> {x}; set C = (B' \ {x}) \/ {x'}; A41: B' \ {x} c= B by A29,XBOOLE_1:43; then A42: C c= B by A37,Th8; not B' c= {x} by A30,A40,ZFMISC_1:39; then A43: B' \ {x} <> {} by XBOOLE_1:37; not x' in B' \ {x} by A35,XBOOLE_0:def 4; then A44: x' in B \(B' \ {x}) by A37,XBOOLE_0:def 4; B' \/ {x'} = B' \/ {x} \/ {x'} by A36,ZFMISC_1:46 .= (B' \ {x}) \/ {x} \/ {x'} by XBOOLE_1:39 .= C \/ {x} by XBOOLE_1:4; hence J.(B' \/ {x'}) = F.(G.C, f.x) by A25,A42 .= F.(F.(G.(B'\{x}), f.x'), f.x) by A15,A41,A43,A44 .= F.(G.(B'\{x}),F.(f.x', f.x)) by A3,BINOP_1:def 3 .= F.(G.(B'\{x}),F.(f.x, f.x')) by A2,BINOP_1:def 2 .= F.(F.(G.(B'\{x}), f.x), f.x') by A3,BINOP_1:def 3 .= F.(J.((B'\{x})\/{x}), f.x') by A25,A41,A43 .= F.(J.(B' \/ {x}), f.x') by XBOOLE_1:39 .= F.(J.B', f.x') by A36,ZFMISC_1:46; end; hence J.(B' \/ {x'}) = F.(J.B', f.x'); suppose A45: not x in B'; then A46: B' c= B by A29,Th5; A47: not ex C being Element of Fin X st C <> {} & C c= B & B' = C \/ {x} by A45,Th6; now per cases; suppose A48: x <> x'; then x' in B by A35,Th6; then A49: x' in B \ B' by A35,XBOOLE_0:def 4; not x in B' \/ {x'} by A45,A48,Th6; then not ex C being Element of Fin X st C <> {} & C c= B & B' \/ {x'} = C \/ {x} by Th6; hence J.(B' \/ {x'}) = G.(B' \/ {x'}) by A25 .= F.(G.B', f.x') by A15,A30,A46,A49 .= F.(J.B', f.x') by A25,A47; suppose x = x'; hence J.(B' \/ {x'}) = F.(G.B', f.x') by A25,A30,A46 .= F.(J.B', f.x') by A25,A47; end; hence J.(B' \/ {x'}) = F.(J.B', f.x'); end; hence thesis; end; end; for B being Element of Fin X holds X[B] from FinSubInd1(A4,A12); then consider G being Function of Fin X, Y such that A50: (for e being Element of Y st e is_a_unity_wrt F holds G.{} = e) & (for x being Element of X holds G.{x} = f.x) & for B' being Element of Fin X st B' c= B & B' <> {} for x being Element of X st x in B \ B' holds G.(B' \/ {x}) = F.(G.B', f.x); take G.B, G; thus thesis by A50; end; uniqueness proof let x,y be Element of Y; given G1 being Function of Fin X, Y such that A51: x = G1.B and A52: for e being Element of Y st e is_a_unity_wrt F holds G1.{} = e and A53: for x being Element of X holds G1.{x} = f.x and A54: for B' being Element of Fin X st B' c= B & B' <> {} for x being Element of X st x in B \ B' holds G1.(B' \/ {x}) = F.(G1.B',f.x); given G2 being Function of Fin X, Y such that A55: y = G2.B and A56: for e being Element of Y st e is_a_unity_wrt F holds G2.{} = e and A57: for x being Element of X holds G2.{x} = f.x and A58: for B' being Element of Fin X st B' c= B & B' <> {} for x being Element of X st x in B \ B' holds G2.(B' \/ {x}) = F.(G2.B',f.x); now per cases; suppose A59: B = {}; then A60: the_unity_wrt F is_a_unity_wrt F by A1,Th22; hence x = the_unity_wrt F by A51,A52,A59 .= y by A55,A56,A59,A60; suppose A61: B <> {}; defpred X[set] means $1 c= B & $1 <> {} implies G1.$1 = G2.$1; A62: X[{}.X]; A63: for B' being Element of Fin X, b being Element of X holds X[B'] & not b in B' implies X[B' \/ {b}] proof let B' be (Element of Fin X), x be Element of X; assume A64: B' c= B & B' <> {} implies G1.B' = G2.B'; assume A65: not x in B'; assume B' \/ {x} c= B; then A66: B' c= B & x in B by Th8; then A67: x in B \ B' by A65,XBOOLE_0:def 4; assume B' \/ {x} <> {}; now per cases; suppose A68: B' = {}; hence G1.(B' \/ {x}) = f.x by A53 .= G2.(B' \/ {x}) by A57,A68; suppose A69: B' <> {}; hence G1.(B' \/ {x}) = F.(G1.B', f.x) by A54,A66,A67 .= G2.(B' \/ {x}) by A58,A64,A66,A67,A69; end; hence G1.(B' \/ {x}) = G2.(B' \/ {x}); end; for B' being Element of Fin X holds X[B'] from FinSubInd1(A62,A63); hence x = y by A51,A55,A61; end; hence thesis; end; end; canceled; theorem Th25: for X, Y being non empty set for F being BinOp of Y for B being Element of Fin X for f being Function of X,Y st (B <> {} or F has_a_unity) & F is idempotent & F is commutative & F is associative for IT being Element of Y holds IT = F $$ (B,f) iff ex G being Function of Fin X, Y st IT = G.B & (for e being Element of Y st e is_a_unity_wrt F holds G.{} = e) & (for x being Element of X holds G.{x} = f.x) & for B' being Element of Fin X st B' c= B & B' <> {} for x being Element of X st x in B holds G.(B' \/ {x}) = F.(G.B',f.x) proof let X, Y be non empty set; let F be BinOp of Y; let B be Element of Fin X; let f be Function of X,Y; assume that A1: B <> {} or F has_a_unity and A2: F is idempotent and A3: F is commutative and A4: F is associative; let IT be Element of Y; thus IT = F $$ (B,f) implies ex G being Function of Fin X, Y st IT = G.B & (for e being Element of Y st e is_a_unity_wrt F holds G.{} = e) & (for x being Element of X holds G.{x} = f.x) & for B' being Element of Fin X st B' c= B & B' <> {} for x being Element of X st x in B holds G.(B' \/ {x}) = F.(G.B',f.x) proof assume IT = F $$ (B,f); then consider G being Function of Fin X, Y such that A5: IT = G.B and A6: for e being Element of Y st e is_a_unity_wrt F holds G.{} = e and A7: for x being Element of X holds G.{x} = f.x and A8: for B' being Element of Fin X st B' c= B & B' <> {} for x being Element of X st x in B \ B' holds G.(B' \/ {x}) = F.(G.B',f.x) by A1,A3,A4,Def3; for B' being Element of Fin X st B' c= B & B' <> {} for x being Element of X st x in B holds G.(B' \/ {x}) = F.(G.B',f.x) proof let B' be Element of Fin X such that A9: B' c= B & B' <> {}; let x be Element of X such that A10: x in B; B' \ {x} c= B' by XBOOLE_1:36; then A11: B' \ {x} c= B by A9,XBOOLE_1:1; now per cases; suppose x in B'; then A12: B' \/ {x} = B' by ZFMISC_1:46; then A13: {x} c= B' by XBOOLE_1:7; not x in B' \ {x} by ZFMISC_1:64; then A14: x in B \ (B' \ {x}) by A10,XBOOLE_0:def 4; now per cases; suppose A15: B' = {x}; hence G.(B' \/ {x}) = f.x by A7 .= F.(f.x, f.x) by A2,BINOP_1:def 4 .= F.(G.B',f.x) by A7,A15; suppose B' <> {x}; then not B' c= {x} by A13,XBOOLE_0:def 10; then B' \ {x} <> {} by XBOOLE_1:37; then A16: G.(B' \ {x} \/ {x}) = F.(G.(B' \ {x}), f.x) by A8,A11,A14; thus G.(B' \/ {x}) = G.(B' \ {x} \/ {x}) by XBOOLE_1:39 .= F.(G.(B' \ {x}), F.(f.x,f.x)) by A2,A16,BINOP_1:def 4 .= F.(F.(G.(B' \ {x}),f.x), f.x) by A4,BINOP_1:def 3 .= F.(G.B',f.x) by A12,A16,XBOOLE_1:39; end; hence G.(B' \/ {x}) = F.(G.B',f.x); suppose not x in B'; then x in B \ B' by A10,XBOOLE_0:def 4; hence G.(B' \/ {x}) = F.(G.B',f.x) by A8,A9; end; hence G.(B' \/ {x}) = F.(G.B',f.x); end; hence thesis by A5,A6,A7; end; given G being Function of Fin X, Y such that A17: IT = G.B and A18: for e being Element of Y st e is_a_unity_wrt F holds G.{} = e and A19: for x being Element of X holds G.{x} = f.x and A20: for B' being Element of Fin X st B' c= B & B' <> {} for x being Element of X st x in B holds G.(B' \/ {x}) = F.(G.B',f.x); for B' being Element of Fin X st B' c= B & B' <> {} for x being Element of X st x in B \ B' holds G.(B' \/ {x}) = F.(G.B',f.x) proof let B' be Element of Fin X such that A21: B' c= B & B' <> {}; let x be Element of X; assume x in B \ B'; then x in B by XBOOLE_0:def 4; hence G.(B' \/ {x}) = F.(G.B',f.x) by A20,A21; end; hence IT = F $$ (B,f) by A1,A3,A4,A17,A18,A19,Def3; end; reserve X, Y for non empty set, F for (BinOp of Y), B for (Element of Fin X), f for Function of X,Y; theorem Th26: F is commutative & F is associative implies for b being Element of X holds F $$ ({b},f) = f.b proof assume A1: F is commutative & F is associative; let b be Element of X; ex G being Function of Fin X, Y st F $$ ({b},f) = G.{b} & (for e being Element of Y st e is_a_unity_wrt F holds G.{} = e) & ( for x being Element of X holds G.{x} = f.x) & for B' being Element of Fin X st B' c= {b} & B' <> {} for x being Element of X st x in {b} \ B' holds G.(B' \/ {x}) = F.(G.B',f.x) by A1,Def3; hence F $$ ({b},f) = f.b; end; theorem Th27: F is idempotent & F is commutative & F is associative implies for a,b being Element of X holds F $$ ({a,b},f) = F.(f.a, f.b) proof assume A1: F is idempotent & F is commutative & F is associative; let a,b be Element of X; consider G being Function of Fin X, Y such that A2: F $$ ({a,b},f) = G.{a,b} and for e being Element of Y st e is_a_unity_wrt F holds G.{} = e and A3: for x being Element of X holds G.{x} = f.x and A4: for B' being Element of Fin X st B' c= {a,b} & B' <> {} for x being Element of X st x in {a,b} holds G.(B' \/ {x}) = F.(G.B',f.x) by A1,Th25; A5: {a} c= {a,b} by ZFMISC_1:12; A6: b in {a,b} by TARSKI:def 2; thus F $$ ({a,b},f) = G.({a} \/ {b}) by A2,ENUMSET1:41 .= F.(G.{a}, f.b) by A4,A5,A6 .= F.(f.a, f.b) by A3; end; theorem Th28: F is idempotent & F is commutative & F is associative implies for a,b,c being Element of X holds F $$ ({a,b,c},f) = F.(F.(f.a, f.b), f.c) proof assume A1: F is idempotent & F is commutative & F is associative; let a,b,c be Element of X; { a,b,c } <> {} by ENUMSET1:14; then consider G being Function of Fin X, Y such that A2: F $$ ({a,b,c},f) = G.{a,b,c} and for e being Element of Y st e is_a_unity_wrt F holds G.{} = e and A3: for x being Element of X holds G.{x} = f.x and A4: for B' being Element of Fin X st B' c= {a,b,c} & B' <> {} for x being Element of X st x in {a,b,c} holds G.(B' \/ {x}) = F.(G.B',f.x) by A1,Th25; A5: {a} c= {a,b,c} by Th3; A6: b in {a,b,c} by ENUMSET1:14; A7: G.{a,b} = G.({a} \/ {b}) by ENUMSET1:41 .= F.(G.{a}, f.b) by A4,A5,A6 .= F.(f.a, f.b) by A3; A8: {a,b} c= {a,b,c} by Th4; A9: c in {a,b,c} by ENUMSET1:14; thus F $$ ({a,b,c},f) = G.({a,b} \/ {c}) by A2,ENUMSET1:43 .= F.(F.(f.a, f.b), f.c) by A4,A7,A8,A9; end; :: I f B i s n o n e m p t y theorem Th29: F is idempotent & F is commutative & F is associative & B <> {} implies for x being Element of X holds F $$(B \/ {x}, f) = F.(F $$(B,f),f.x) proof assume A1: F is idempotent & F is commutative & F is associative; assume A2: B <> {}; let x be Element of X; consider G being Function of Fin X, Y such that A3: F $$ (B \/ {x},f) = G.(B \/ {x}) and for e being Element of Y st e is_a_unity_wrt F holds G.{} = e and A4: for x being Element of X holds G.{x} = f.x and A5: for B' being Element of Fin X st B' c= B \/ {x} & B' <> {} for x' being Element of X st x' in B \/ {x} holds G.(B' \/ {x'}) = F.(G.B',f.x') by A1,Th25; consider G' being Function of Fin X, Y such that A6: F $$ (B,f) = G'.B and for e being Element of Y st e is_a_unity_wrt F holds G'.{} = e and A7: for x being Element of X holds G'.{x} = f.x and A8: for B' being Element of Fin X st B' c= B & B' <> {} for x being Element of X st x in B holds G'.(B' \/ {x}) = F.(G'.B',f.x) by A1,A2,Th25; defpred X[set] means $1 <> {} & $1 c= B implies G.$1 = G'.$1; A9: X[{}.X]; A10: for B' being Element of Fin X, b being Element of X holds X[B'] implies X[B' \/ {b}] proof let C be (Element of Fin X), y be Element of X such that A11: C <> {} & C c= B implies G.C = G'.C; assume that C \/ {y} <> {} and A12: C \/ {y} c= B; A13: C c= B & y in B by A12,Th8; A14: B c= B \/ {x} by XBOOLE_1:7; then A15: C c= B \/ {x} by A13,XBOOLE_1:1; now per cases; suppose A16: C = {}; hence G.(C \/ {y}) = f.y by A4 .= G'.(C \/ {y}) by A7,A16; suppose A17: C <> {}; hence G.(C \/ {y}) = F.(G'.C, f.y) by A5,A11,A13,A14,A15 .= G'.(C \/ {y}) by A8,A13,A17; end; hence G.(C \/ {y}) = G'.(C \/ {y}); end; A18: for C being Element of Fin X holds X[C] from FinSubInd3(A9,A10); A19: B c= B \/ {x} by XBOOLE_1:7; x in B \/ {x} by Th6; hence F $$(B \/ {x}, f) = F.(G.B, f.x) by A2,A3,A5,A19 .= F.(F $$(B,f),f.x) by A2,A6,A18; end; theorem Th30: F is idempotent & F is commutative & F is associative implies for B1,B2 being Element of Fin X st B1 <> {} & B2 <> {} holds F $$ (B1 \/ B2,f) = F.(F $$ (B1,f),F $$ (B2,f)) proof assume A1: F is idempotent & F is commutative & F is associative; let B1,B2 be Element of Fin X; assume A2: B1 <> {}; defpred X[Element of Fin X] means $1 <> {} implies F $$ (B1 \/ $1,f) = F.(F $$ (B1,f),F $$ ($1,f)); A3: X[{}.X]; A4: for B' being Element of Fin X, b being Element of X holds X[B'] implies X[B' \/ {b}] proof let B be (Element of Fin X), x be Element of X such that A5: B <> {} implies F $$ (B1 \/ B,f) = F.(F $$ (B1,f),F $$ (B,f)) and B \/ {x} <> {}; now per cases; suppose A6: B = {}; hence F $$ (B1 \/ (B \/ {x}),f) = F.(F $$ (B1,f), f.x) by A1,A2,Th29 .= F.(F $$ (B1,f),F $$ (B \/ {x},f)) by A1,A6,Th26; suppose A7: B <> {}; then A8: B1 \/ B <> {} by XBOOLE_1:15; thus F $$ (B1 \/ (B \/ {x}),f) = F $$ (B1 \/ B \/ {x},f) by XBOOLE_1:4 .= F.(F.(F $$ (B1,f),F $$ (B,f)), f.x) by A1,A5,A7,A8,Th29 .= F.(F $$ (B1,f),F.(F $$ (B,f), f.x)) by A1,BINOP_1:def 3 .= F.(F $$ (B1,f),F $$ (B \/ {x},f)) by A1,A7,Th29; end; hence F $$ (B1 \/ (B \/ {x}),f) = F.(F $$ (B1,f),F $$ (B \/ {x},f)); end; for B2 being Element of Fin X holds X[B2] from FinSubInd3(A3,A4); hence thesis; end; theorem F is commutative & F is associative & F is idempotent implies for x being Element of X st x in B holds F.(f.x,F$$(B,f)) = F$$(B,f) proof assume A1: F is commutative & F is associative & F is idempotent; let x be Element of X; assume A2: x in B; thus F.(f.x,F$$(B,f)) = F.(F$$({x},f), F$$(B,f)) by A1,Th26 .= F$$({x} \/ B, f) by A1,A2,Th30 .= F$$(B,f) by A2,ZFMISC_1:46; end; theorem F is commutative & F is associative & F is idempotent implies for B,C being Element of Fin X st B <> {} & B c= C holds F.(F$$(B,f),F$$(C,f)) = F$$(C,f) proof assume A1: F is commutative & F is associative & F is idempotent; let B,C be Element of Fin X such that A2: B <> {} and A3: B c= C; C <> {} by A2,A3,XBOOLE_1:3; hence F.(F$$(B,f),F$$(C,f)) = F$$(B \/ C,f) by A1,A2,Th30 .= F$$(C,f) by A3,XBOOLE_1:12; end; theorem Th33: B <> {} & F is commutative & F is associative & F is idempotent implies for a being Element of Y st for b being Element of X st b in B holds f.b = a holds F$$(B,f) = a proof assume that A1: B <> {} and A2: F is commutative & F is associative & F is idempotent; let a be Element of Y; defpred X[Element of Fin X] means (for b being Element of X st b in $1 holds f.b = a) implies F$$($1,f) = a; A3: for x being Element of X holds X[{x}] proof let x be Element of X such that A4: for b being Element of X st b in {x} holds f.b = a; A5: x in { x } by TARSKI:def 1; thus F$$({x},f) = f.x by A2,Th26 .= a by A4,A5; end; A6: for B1,B2 being Element of Fin X st B1 <> {} & B2 <> {} holds X[B1] & X[B2] implies X[B1 \/ B2] proof let B1,B2 be Element of Fin X such that A7: B1 <> {} & B2 <> {}; assume that A8: (for b being Element of X st b in B1 holds f.b = a) implies F$$(B1,f) = a and A9: (for b being Element of X st b in B2 holds f.b = a) implies F$$(B2,f) = a and A10: for b being Element of X st b in B1 \/ B2 holds f.b = a; A11: now let b be Element of X; assume b in B1; then b in B1 \/ B2 by XBOOLE_0:def 2 ; hence f.b = a by A10; end; now let b be Element of X; assume b in B2; then b in B1 \/ B2 by XBOOLE_0:def 2 ; hence f.b = a by A10; end; hence F$$(B1 \/ B2,f) = F.(a,a) by A2,A7,A8,A9,A11,Th30 .= a by A2,BINOP_1:def 4; end; for B being Element of Fin X st B<>{} holds X[B] from FinSubInd2(A3,A6); hence thesis by A1; end; theorem Th34: F is commutative & F is associative & F is idempotent implies for a being Element of Y st f.:B = {a} holds F$$(B,f) = a proof assume A1: F is commutative & F is associative & F is idempotent; let a be Element of Y; assume A2: f.:B = {a}; then A3: B <> {} by RELAT_1:149; for b being Element of X st b in B holds f.b = a proof let b be Element of X; assume b in B; then f.b in {a} by A2,FUNCT_2:43; hence f.b = a by TARSKI:def 1; end; hence F$$(B,f) = a by A1,A3,Th33; end; theorem Th35: F is commutative & F is associative & F is idempotent implies for f,g being Function of X,Y for A,B being Element of Fin X st A <> {} & f.:A = g.:B holds F$$(A,f) = F$$(B,g) proof assume A1: F is commutative & F is associative & F is idempotent; let f,g be Function of X,Y; let A,B be Element of Fin X such that A2: A <> {} and A3: f.:A = g.:B; defpred X[Element of Fin X] means $1 <> {} implies for B being Element of Fin X st f.:$1 = g.:B holds F$$($1,f) = F$$(B,g); A4: X[{}.X]; A5: for B' being Element of Fin X, b being Element of X holds X[B'] implies X[B' \/ {b}] proof let A be (Element of Fin X), x be Element of X such that A6: A <> {} implies for B being Element of Fin X st f.:A = g.:B holds F$$(A,f) = F$$(B,g); assume A \/ {x} <> {}; let B be Element of Fin X such that A7: f.:(A \/ {x}) = g.:B; now per cases; suppose f.x in f.:A; then consider x' being Element of X such that A8: x' in A and A9: f.x' = f.x by FUNCT_2:116; A10: f.x in f.:A by A8,A9,FUNCT_2:43; A11: g.:B = f.:A \/ f.:{x} by A7,RELAT_1:153 .= f.:A \/ {f.x} by Th13 .= f.:A by A10,ZFMISC_1:46; thus F$$(A \/ {x},f) = F.(F$$(A,f), f.x) by A1,A8,Th29 .= F.(F$$(A \/ {x'},f), f.x) by A8,ZFMISC_1:46 .= F.(F.(F$$(A,f), f.x'), f.x) by A1,A8,Th29 .= F.(F$$(A,f), F.(f.x', f.x')) by A1,A9,BINOP_1:def 3 .= F.(F$$(A,f), f.x') by A1,BINOP_1:def 4 .= F$$(A \/ {x'},f) by A1,A8,Th29 .= F$$(A,f) by A8,ZFMISC_1:46 .= F$$(B,g) by A6,A8,A11; suppose A12: not f.x in f.:A; now per cases; suppose A13: A = {}; then A14: g.:B = {f.x} by A7,Th13; thus F$$(A \/ {x},f) = f.x by A1,A13,Th26 .= F$$(B,g) by A1,A14,Th34; suppose A15: A <> {}; B /\ g"{f.x} c= B by XBOOLE_1:17; then reconsider B2 = B /\ g"{f.x} as Element of Fin X by Th16; B \ g"{f.x} c= B by XBOOLE_1:36; then reconsider B1 = B \ g"{f.x} as Element of Fin X by Th16; A16: B = B1 \/ B2 by XBOOLE_1:51; A17: now assume B1 = {}; then B c= g"{f.x} by XBOOLE_1:37; then A18: g.:B c= g.:g"{f.x} by RELAT_1:156; A19: f.:A misses {f.x} by A12,ZFMISC_1:56; g.:g"{f.x} c= {f.x} by FUNCT_1:145; then f.:(A \/ {x}) c= {f.x} by A7,A18,XBOOLE_1:1; then f.:A \/ f.:{x} c= {f.x} by RELAT_1:153; then f.:A c= {f.x} by XBOOLE_1:11; then f.:A = f.:A /\ {f.x} by XBOOLE_1:28 .= {} by A19,XBOOLE_0:def 7; hence contradiction by A15,Th19; end; x in A \/ {x} by Th6; then f.x in g.:B by A7,FUNCT_2:43; then consider x' being Element of X such that A20: x' in B and A21: g.x' = f.x by FUNCT_2:116; x' in g"{f.x} by A21,Th12; then A22: B2 <> {} by A20,XBOOLE_0:def 3; A23: f.:A = f.:A \ {f.x} by A12,ZFMISC_1:65 .= f.:A \ f.:{x} by Th13 .= (f.:A \/ f.:{x}) \ f.:{x} by XBOOLE_1:40 .= f.:(A \/ {x}) \ f.:{x} by RELAT_1:153 .= g.:B \ {f.x} by A7,Th13 .= g.:B1 by Th11; A24: for b being Element of X st b in B2 holds g.b = f.x proof let b be Element of X; assume b in B2; then b in g"{f.x} by XBOOLE_0:def 3; then g.b in {f.x} by FUNCT_1:def 13; hence g.b = f.x by TARSKI:def 1; end; thus F$$(A \/ {x},f) = F.(F$$(A,f), f.x) by A1,A15,Th29 .= F.(F$$(B1,g), f.x) by A6,A15,A23 .= F.(F$$(B1,g), F$$(B2,g)) by A1,A22,A24,Th33 .= F$$(B,g) by A1,A16,A17,A22,Th30; end; hence F$$(A \/ {x},f) = F$$(B,g); end; hence F$$(A \/ {x},f) = F$$(B,g); end; for A being Element of Fin X holds X[A] from FinSubInd3(A4,A5); hence thesis by A2,A3; end; theorem for F,G being BinOp of Y st F is idempotent & F is commutative & F is associative & G is_distributive_wrt F for B being Element of Fin X st B <> {} for f being Function of X,Y for a being Element of Y holds G.(a,F$$(B,f)) = F$$(B,G[;](a,f)) proof let F,G be BinOp of Y such that A1: F is idempotent & F is commutative & F is associative and A2: G is_distributive_wrt F; let B be Element of Fin X such that A3: B<> {}; let f be Function of X,Y; let a be Element of Y; defpred X[Element of Fin X] means G.(a,F$$($1,f)) = F$$($1,G[;](a,f)); A4: for x being Element of X holds X[{x}] proof let x be Element of X; thus G.(a,F$$({x},f)) = G.(a,f.x) by A1,Th26 .= (G[;](a,f)).x by FUNCOP_1:66 .= F$$({x},G[;](a,f)) by A1,Th26; end; A5: for B1,B2 being Element of Fin X st B1 <> {} & B2 <> {} holds X[B1] & X[B2] implies X[B1 \/ B2] proof let B1,B2 be Element of Fin X such that A6: B1 <> {} & B2 <> {}; assume that A7: G.(a,F$$(B1,f)) = F$$(B1,G[;](a,f)) and A8: G.(a,F$$(B2,f)) = F$$(B2,G[;](a,f)); thus G.(a,F$$(B1 \/ B2,f)) = G.(a,F.(F$$(B1,f),F$$(B2,f))) by A1,A6,Th30 .= F.(F$$(B1,G[;](a,f)), F$$(B2,G[;] (a,f))) by A2,A7,A8,BINOP_1:23 .= F$$(B1 \/ B2,G[;](a,f)) by A1,A6,Th30; end; for B being Element of Fin X st B <> {} holds X[B] from FinSubInd2(A4,A5); hence G.(a,F$$(B,f)) = F$$(B,G[;](a,f)) by A3; end; theorem for F,G being BinOp of Y st F is idempotent & F is commutative & F is associative & G is_distributive_wrt F for B being Element of Fin X st B <> {} for f being Function of X,Y for a being Element of Y holds G.(F$$(B,f),a) = F$$(B,G[:](f,a)) proof let F,G be BinOp of Y such that A1: F is idempotent & F is commutative & F is associative and A2: G is_distributive_wrt F; let B be Element of Fin X such that A3: B<> {}; let f be Function of X,Y; let a be Element of Y; defpred X[Element of Fin X] means G.(F$$($1,f),a) = F$$($1,G[:](f,a)); A4: for x being Element of X holds X[{x}] proof let x be Element of X; thus G.(F$$({x},f),a) = G.(f.x,a) by A1,Th26 .= (G[:](f,a)).x by FUNCOP_1:60 .= F$$({x},G[:](f,a)) by A1,Th26; end; A5: for B1,B2 being Element of Fin X st B1 <> {} & B2 <> {} holds X[B1] & X[B2] implies X[B1 \/ B2] proof let B1,B2 be Element of Fin X such that A6: B1 <> {} & B2 <> {}; assume that A7: G.(F$$(B1,f),a) = F$$(B1,G[:](f,a)) and A8: G.(F$$(B2,f),a) = F$$(B2,G[:](f,a)); thus G.(F$$(B1 \/ B2,f),a) = G.(F.(F$$(B1,f),F$$(B2,f)),a) by A1,A6,Th30 .= F.(F$$(B1,G[:](f,a)), F$$(B2,G[:] (f,a))) by A2,A7,A8,BINOP_1:23 .= F$$(B1 \/ B2,G[:](f,a)) by A1,A6,Th30; end; for B being Element of Fin X st B <> {} holds X[B] from FinSubInd2(A4,A5); hence G.(F$$(B,f),a) = F$$(B,G[:](f,a)) by A3; end; definition let X, Y be non empty set; let f be Function of X,Y; let A be Element of Fin X; redefine func f.:A -> Element of Fin Y; coherence by Lm1; end; theorem Th38: for A, X, Y being non empty set for F being BinOp of A st F is idempotent & F is commutative & F is associative for B being Element of Fin X st B <> {} for f being Function of X,Y holds for g being Function of Y,A holds F$$(f.:B,g) = F$$(B,g*f) proof let A, X, Y be non empty set, F be BinOp of A such that A1: F is idempotent & F is commutative & F is associative; let B be Element of Fin X such that A2: B <> {}; let f be Function of X,Y; let g be Function of Y,A; A3: dom f = X by FUNCT_2:def 1; defpred X[Element of Fin X] means F$$(f.:$1,g) = F$$($1,g*f); A4: for x being Element of X holds X[{x}] proof let x be Element of X; thus F$$(f.:{x},g) = F$$({f.x},g) by A3,FUNCT_1:117 .= g.(f.x) by A1,Th26 .= (g*f).x by FUNCT_2:21 .= F$$({x},g*f) by A1,Th26; end; A5: for B1,B2 being Element of Fin X st B1 <> {} & B2 <> {} holds X[B1] & X[B2] implies X[B1 \/ B2] proof let B1,B2 be Element of Fin X such that A6: B1 <> {} & B2 <> {}; B1 c= X & B2 c= X by FINSUB_1:def 5; then X /\ B1 <> {} & X /\ B2 <> {} by A6,XBOOLE_1:28; then X meets B1 & X meets B2 by XBOOLE_0:def 7; then A7: f.:B1 <> {} & f.:B2 <> {} by A3,RELAT_1:151; assume A8: F$$(f.:B1,g) = F$$(B1,g*f) & F$$(f.:B2,g) = F$$(B2,g*f); thus F$$(f.:(B1 \/ B2),g) = F$$(f.:B1 \/ f.:B2, g) by RELAT_1:153 .= F.(F$$(f.:B1,g), F$$(f.:B2,g)) by A1,A7,Th30 .= F$$(B1 \/ B2,g*f) by A1,A6,A8,Th30; end; for B being Element of Fin X st B <> {} holds X[B] from FinSubInd2(A4,A5); hence F$$(f.:B,g) = F$$(B,g*f) by A2; end; theorem Th39: F is commutative & F is associative & F is idempotent implies for Z being non empty set for G being BinOp of Z st G is commutative & G is associative & G is idempotent for f being Function of X, Y for g being Function of Y,Z st for x,y being Element of Y holds g.(F.(x,y)) = G.(g.x,g.y) for B being Element of Fin X st B <> {} holds g.(F$$(B,f)) = G$$(B,g*f) proof assume A1: F is commutative & F is associative & F is idempotent; let Z be non empty set, G be BinOp of Z such that A2: G is commutative & G is associative & G is idempotent; let f be Function of X,Y; let g be Function of Y,Z such that A3: for x,y being Element of Y holds g.(F.(x, y)) = G.(g.x, g.y); defpred X[Element of Fin X] means $1 <> {} implies g.(F$$($1,f)) = G$$($1,g*f); A4: X[{}.X]; A5: for B' being Element of Fin X, b being Element of X holds X[B'] implies X[B' \/ {b}] proof let B be (Element of Fin X), x be Element of X; assume that A6: B <> {} implies g.(F$$(B,f)) = G$$(B,g*f) and B \/ {x} <> {}; now per cases; suppose A7: B = {}; hence g.(F$$(B \/ {x},f)) = g.(f.x) by A1,Th26 .= (g*f).x by FUNCT_2:21 .= G$$(B \/ {x},g*f) by A2,A7,Th26; suppose A8: B <> {}; hence g.(F$$(B \/ {x},f)) = g.(F.(F$$(B,f), f.x)) by A1,Th29 .= G.(g.(F$$(B,f)), g.(f.x)) by A3 .= G.(G$$(B,g*f), (g*f).x) by A6,A8,FUNCT_2:21 .= G$$(B \/ {x},g*f) by A2,A8,Th29; end; hence g.(F$$(B \/ {x},f)) = G$$(B \/ {x},g*f); end; thus for B being Element of Fin X holds X[B] from FinSubInd3(A4,A5); end; :: I f F h a s a u n i t y theorem Th40: F is commutative & F is associative & F has_a_unity implies for f holds F$$({}.X,f) = the_unity_wrt F proof assume that A1: F is commutative & F is associative and A2: F has_a_unity; let f; A3: the_unity_wrt F is_a_unity_wrt F & {} = {}.X by A2,Th22; ex G being Function of Fin X, Y st F $$ ({}.X,f) = G.{}.X & (for e being Element of Y st e is_a_unity_wrt F holds G.{} = e) & (for x being Element of X holds G.{x} = f.x) & for B' being Element of Fin X st B' c= {}.X & B' <> {} for x being Element of X st x in {}.X \ B' holds G.(B' \/ {x}) = F.(G.B',f.x) by A1,A2,Def3; hence F$$({}.X,f) = the_unity_wrt F by A3; end; theorem Th41: F is idempotent & F is commutative & F is associative & F has_a_unity implies for x being Element of X holds F $$(B \/ {x}, f) = F.(F $$(B,f),f.x) proof assume A1: F is idempotent & F is commutative & F is associative; assume A2: F has_a_unity; A3: {} = {}.X; let x be Element of X; now assume A4: B = {}; hence F $$(B \/ {x}, f) = f.x by A1,Th26 .= F.(the_unity_wrt F, f.x) by A2,Th23 .= F.(F $$(B,f),f.x) by A1,A2,A3,A4,Th40; end; hence thesis by A1,Th29; end; theorem F is idempotent & F is commutative & F is associative & F has_a_unity implies for B1,B2 being Element of Fin X holds F $$ (B1 \/ B2,f) = F.(F $$ (B1,f),F $$ (B2,f)) proof assume that A1: F is idempotent & F is commutative & F is associative and A2: F has_a_unity; let B1,B2 be Element of Fin X; now assume A3: B1 = {} or B2 = {}; A4: {} = {}.X; now per cases by A3; suppose A5: B2 = {}; hence F $$ (B1 \/ B2,f) = F.(F$$(B1,f),the_unity_wrt F) by A2,Th23 .= F.(F $$ (B1,f),F $$ (B2,f)) by A1,A2,A4,A5,Th40; suppose A6: B1 = {}; hence F $$ (B1 \/ B2,f) = F.(the_unity_wrt F, F$$(B2,f)) by A2,Th23 .= F.(F $$ (B1,f),F $$ (B2,f)) by A1,A2,A4,A6,Th40; end; hence thesis; end; hence thesis by A1,Th30; end; theorem F is commutative & F is associative & F is idempotent & F has_a_unity implies for f,g being Function of X,Y for A,B being Element of Fin X st f.:A = g.:B holds F$$(A,f) = F$$(B,g) proof assume that A1: F is commutative & F is associative & F is idempotent and A2: F has_a_unity; let f,g be Function of X,Y; let A,B be Element of Fin X such that A3: f.:A = g.:B; now assume A = {}; then f.:A = {} by RELAT_1:149; then A = {}.X & B = {}.X by A3,Th19; then F$$(A,f) = the_unity_wrt F & F$$(B,g) = the_unity_wrt F by A1,A2, Th40; hence thesis; end; hence thesis by A1,A3,Th35; end; theorem Th44: for A, X, Y being non empty set for F being BinOp of A st F is idempotent & F is commutative & F is associative & F has_a_unity for B being Element of Fin X for f being Function of X,Y holds for g being Function of Y,A holds F$$(f.:B,g) = F$$(B,g*f) proof let A, X, Y be non empty set, F be BinOp of A such that A1: F is idempotent & F is commutative & F is associative and A2: F has_a_unity; let B be Element of Fin X; let f be Function of X,Y; let g be Function of Y,A; now assume B = {}; then B = {}.X & f.:B = {}.Y by RELAT_1:149; then F$$(f.:B,g) = the_unity_wrt F & F$$(B,g*f) = the_unity_wrt F by A1,A2,Th40; hence thesis; end; hence F$$(f.:B,g) = F$$(B,g*f) by A1,Th38; end; theorem F is commutative & F is associative & F is idempotent & F has_a_unity implies for Z being non empty set for G being BinOp of Z st G is commutative & G is associative & G is idempotent & G has_a_unity for f being Function of X, Y for g being Function of Y,Z st g.the_unity_wrt F = the_unity_wrt G & for x,y being Element of Y holds g.(F.(x,y)) = G.(g.x,g.y) for B being Element of Fin X holds g.(F$$(B,f)) = G$$(B,g*f) proof assume A1: F is commutative & F is associative & F is idempotent & F has_a_unity; let Z be non empty set; let G be BinOp of Z such that A2: G is commutative & G is associative & G is idempotent & G has_a_unity; let f be Function of X, Y; let g be Function of Y,Z such that A3: g.the_unity_wrt F = the_unity_wrt G and A4: for x,y being Element of Y holds g.(F.(x,y)) = G.(g.x,g.y); let B be Element of Fin X; now per cases; suppose B = {}; then A5: B = {}.X; hence g.(F$$(B,f)) = g.the_unity_wrt F by A1,Th40 .= G$$(B,g*f) by A2,A3,A5,Th40; suppose B <> {}; hence g.(F$$(B,f)) = G$$(B,g*f) by A1,A2,A4,Th39; end; hence g.(F$$(B,f)) = G$$(B,g*f); end; :: Funkcja wprowadzona powyzej konieczna jest do zakastowania :: wyniku operacji unii. Jest to Element of DOMAIN , :: co nie rozszerza sie do Element of DOMAIN definition let A be set; func FinUnion A -> BinOp of Fin A means :Def4: for x,y being Element of Fin A holds it.(x,y) = (x \/ y); existence proof deffunc U(Element of Fin A,Element of Fin A) = $1 \/ $2; ex IT being BinOp of Fin A st for x,y being Element of Fin A holds IT.(x,y) = U(x,y) from BinOpLambda; hence thesis; end; uniqueness proof let IT, IT' be BinOp of Fin A such that A1: for x,y being Element of Fin A holds IT.(x,y) = (x \/ y) and A2: for x,y being Element of Fin A holds IT'.(x,y) = (x \/ y); now let x,y be Element of Fin A; thus IT.[x,y] = IT.(x,y) by BINOP_1:def 1 .= (x \/ y) by A1 .= IT'.(x,y) by A2 .= IT'.[x,y] by BINOP_1:def 1; end; hence IT = IT' by FUNCT_2:120; end; end; reserve A for set, x,y,z for Element of Fin A; canceled 3; theorem Th49: FinUnion A is idempotent proof let x; thus FinUnion A.(x,x) = x \/ x by Def4 .= x; end; theorem Th50: FinUnion A is commutative proof let x,y; thus FinUnion A.(x,y) = y \/ x by Def4 .= FinUnion A.(y,x) by Def4; end; theorem Th51: FinUnion A is associative proof let x,y,z; thus FinUnion A.(FinUnion A.(x,y), z) = FinUnion A.(x \/ y, z) by Def4 .= x \/ y \/ z by Def4 .= x \/ (y \/ z) by XBOOLE_1:4 .= FinUnion A.(x, y \/ z) by Def4 .= FinUnion A.(x, FinUnion A.(y,z)) by Def4; end; theorem Th52: {}.A is_a_unity_wrt FinUnion A proof thus for x holds FinUnion A.({}.A, x) =x proof let x; thus FinUnion A.({}.A, x) = {} \/ x by Def4 .= x; end; let x; thus FinUnion A.(x, {}.A) = x \/ {} by Def4 .= x; end; theorem Th53: FinUnion A has_a_unity proof {}.A is_a_unity_wrt FinUnion A by Th52; hence thesis by Def2; end; theorem the_unity_wrt FinUnion A is_a_unity_wrt FinUnion A proof FinUnion A has_a_unity by Th53; hence thesis by Th22; end; theorem Th55: the_unity_wrt FinUnion A = {} proof {}.A is_a_unity_wrt FinUnion A by Th52; hence thesis by BINOP_1:def 8; end; reserve X,Y for non empty set, A for set, f for (Function of X, Fin A), i,j,k for (Element of X); definition let X be non empty set, A be set; let B be Element of Fin X; let f be Function of X, Fin A; func FinUnion(B,f) -> Element of Fin A equals :Def5: FinUnion A $$(B,f); correctness; end; theorem FinUnion({i},f) = f.i proof A1: FinUnion A is idempotent & FinUnion A is commutative & FinUnion A is associative by Th49,Th50,Th51; thus FinUnion({i},f) = FinUnion A $$({i},f) by Def5 .= f.i by A1,Th26; end; theorem FinUnion({i,j},f) = f.i \/ f.j proof A1: FinUnion A is idempotent & FinUnion A is commutative & FinUnion A is associative by Th49,Th50,Th51; thus FinUnion({i,j},f) = FinUnion A $$({i,j},f) by Def5 .= FinUnion A.(f.i, f.j) by A1,Th27 .= f.i \/ f.j by Def4; end; theorem FinUnion({i,j,k},f) = f.i \/ f.j \/ f.k proof A1: FinUnion A is idempotent & FinUnion A is commutative & FinUnion A is associative by Th49,Th50,Th51; thus FinUnion({i,j,k},f) = FinUnion A $$({i,j,k},f) by Def5 .= FinUnion A.(FinUnion A.(f.i, f.j), f.k) by A1,Th28 .= FinUnion A.(f.i \/ f.j, f.k) by Def4 .= f.i \/ f.j \/ f.k by Def4; end; theorem Th59: FinUnion({}.X,f) = {} proof A1: FinUnion A is idempotent & FinUnion A is commutative & FinUnion A is associative & FinUnion A has_a_unity by Th49,Th50,Th51,Th53 ; thus FinUnion({}.X,f) = FinUnion A $$({}.X,f) by Def5 .= the_unity_wrt FinUnion A by A1,Th40 .= {} by Th55; end; theorem Th60: for B being Element of Fin X holds FinUnion(B \/ {i}, f) = FinUnion(B,f) \/ f.i proof let B be Element of Fin X; A1: FinUnion A is idempotent & FinUnion A is commutative & FinUnion A is associative & FinUnion A has_a_unity by Th49,Th50,Th51,Th53 ; A2: FinUnion(B,f) = FinUnion A $$(B,f) by Def5; thus FinUnion(B \/ {i}, f) = FinUnion A $$(B \/ {i}, f) by Def5 .= FinUnion A.(FinUnion(B,f), f.i) by A1,A2,Th41 .= FinUnion(B,f) \/ f.i by Def4; end; theorem Th61: for B being Element of Fin X holds FinUnion(B,f) = union (f.:B) proof defpred X[Element of Fin X] means FinUnion($1,f) = union (f.:$1); A1: X[{}.X] proof thus FinUnion({}.X,f) = union {} by Th59,ZFMISC_1:2 .= union (f.:{}.X) by RELAT_1:149; end; A2: for B being (Element of Fin X), i st X[B] holds X[B \/ {i}] proof let B be (Element of Fin X), i; assume FinUnion(B,f) = union (f.:B); hence FinUnion(B \/ {i}, f) = union(f.:B) \/ f.i by Th60 .= union (f.:B) \/ union {f.i} by ZFMISC_1:31 .= union (f.:B \/ {f.i}) by ZFMISC_1:96 .= union (f.:B \/ f.:{i}) by Th13 .= union (f.:(B \/ {i})) by RELAT_1:153; end; thus for B being Element of Fin X holds X[B] from FinSubInd3(A1,A2); end; theorem for B1,B2 being Element of Fin X holds FinUnion(B1 \/ B2, f) = FinUnion(B1,f) \/ FinUnion(B2,f) proof let B1,B2 be Element of Fin X; thus FinUnion(B1 \/ B2, f) = union(f.:(B1 \/ B2)) by Th61 .= union(f.:B1 \/ f .:B2) by RELAT_1:153 .= union(f.:B1) \/ union(f.:B2) by ZFMISC_1:96 .= FinUnion(B1,f) \/ union(f.:B2) by Th61 .= FinUnion(B1,f) \/ FinUnion(B2,f) by Th61; end; theorem for B being Element of Fin X for f being Function of X,Y holds for g being Function of Y,Fin A holds FinUnion(f.:B,g) = FinUnion(B,g*f) proof let B be Element of Fin X; let f be Function of X,Y; let g be Function of Y,Fin A; thus FinUnion(f.:B,g) = union (g.:(f.:B)) by Th61 .= union ((g*f).:B) by RELAT_1:159 .= FinUnion(B,g*f) by Th61; end; theorem Th64: for A,X being non empty set, Y being set for G being BinOp of A st G is commutative & G is associative & G is idempotent for B being Element of Fin X st B <> {} for f being (Function of X,Fin Y), g being Function of Fin Y,A st for x,y being Element of Fin Y holds g.(x \/ y) = G.(g.x,g.y) holds g.(FinUnion(B,f)) = G$$(B,g*f) proof let A,X be non empty set, Y be set, G be BinOp of A such that A1: G is commutative & G is associative & G is idempotent; A2: FinUnion Y is commutative & FinUnion Y is associative & FinUnion Y is idempotent by Th49,Th50,Th51; let B be Element of Fin X such that A3: B <> {}; let f be (Function of X,Fin Y), g be Function of Fin Y,A such that A4: for x,y being Element of Fin Y holds g.(x \/ y) = G.(g.x,g.y); A5: now let x,y be Element of Fin Y; thus g.(FinUnion Y.(x,y)) = g.(x \/ y) by Def4 .= G.(g.x,g.y) by A4; end; thus g.(FinUnion(B,f)) = g.(FinUnion Y $$(B,f)) by Def5 .= G $$(B,g*f) by A1,A2,A3,A5,Th39; end; theorem Th65: for Z being non empty set, Y being set for G being BinOp of Z st G is commutative & G is associative & G is idempotent & G has_a_unity for f being Function of X, Fin Y for g being Function of Fin Y,Z st g.{}.Y = the_unity_wrt G & for x,y being Element of Fin Y holds g.(x \/ y) = G.(g.x,g.y) for B being Element of Fin X holds g.(FinUnion(B,f)) = G$$(B,g*f) proof let Z be non empty set, Y be set; let G be BinOp of Z such that A1: G is commutative & G is associative & G is idempotent & G has_a_unity; let f be Function of X, Fin Y; let g be Function of Fin Y,Z such that A2: g.{}.Y = the_unity_wrt G and A3: for x,y being Element of Fin Y holds g.(x \/ y) = G.(g.x,g.y); let B be Element of Fin X; A4:{} = {}.X; A5: {} = {}.Fin Y; now per cases; suppose A6: B = {}; then A7: f.:B = {} by RELAT_1:149; thus g.(FinUnion(B,f)) = g.{}.Y by A4,A6,Th59 .= G$$(f.:B,g) by A1,A2,A5,A7,Th40 .= G$$(B,g*f) by A1,Th44; suppose B <> {}; hence g.(FinUnion(B,f)) = G$$(B,g*f) by A1,A3,Th64; end; hence g.(FinUnion(B,f)) = G$$(B,g*f); end; definition let A be set; func singleton A -> Function of A, Fin A means :Def6: for x being set st x in A holds it.x = {x}; existence proof deffunc U(set) = {$1}; A1: now let x be set; assume A2: x in A; then reconsider A' = A as non empty set; reconsider x' = x as Element of A' by A2; {x'} in Fin A'; hence U(x) in Fin A; end; thus ex f being Function of A, Fin A st for x being set st x in A holds f.x = U(x) from Lambda1(A1); end; uniqueness proof let IT,IT' be Function of A, Fin A such that A3: for x being set st x in A holds IT.x = {x} and A4: for x being set st x in A holds IT'.x = {x}; now let x be set; assume x in A; then IT.x = {x} & IT'.x = {x} by A3,A4; hence IT.x = IT'.x; end; hence thesis by FUNCT_2:18; end; end; canceled; theorem Th67: for A being non empty set for f being Function of A, Fin A holds f = singleton A iff for x being Element of A holds f.x = {x} proof let A be non empty set; let f be Function of A, Fin A; thus f = singleton A implies for x being Element of A holds f.x = {x} by Def6; assume for x being Element of A holds f.x = {x}; then for x be set holds x in A implies f.x = {x}; hence f = singleton A by Def6; end; theorem Th68: for x being set, y being Element of X holds x in singleton X.y iff x = y proof let x be set, y be Element of X; singleton X.y = {y} by Th67; hence x in singleton X.y iff x = y by TARSKI:def 1; end; theorem for x,y,z being Element of X st x in singleton X.z & y in singleton X.z holds x = y proof let x,y,z be Element of X; assume x in singleton X.z & y in singleton X.z; then x = z & y = z by Th68; hence x = y; end; Lm2: for D being non empty set, X, P being set for f being Function of X,D holds f.:P c= D; theorem Th70: for B being Element of Fin X, x being set holds x in FinUnion(B, f) iff ex i being Element of X st i in B & x in f.i proof let B be Element of Fin X, x be set; A1: now assume x in union (f.:B); then consider Z being set such that A2: x in Z and A3: Z in f .:B by TARSKI:def 4; f.:B is Subset of Fin A by Lm2; then reconsider Z as Element of Fin A by A3; consider i being Element of X such that A4: i in B & Z = f.i by A3,FUNCT_2:116; take i' = i; thus i' in B & x in f.i' by A2,A4; end; now given i being Element of X such that A5: i in B & x in f.i; f.i in f.:B by A5,FUNCT_2:43; hence x in union (f.:B) by A5,TARSKI:def 4; end; hence thesis by A1,Th61; end; theorem for B being Element of Fin X holds FinUnion(B, singleton X) = B proof let B be Element of Fin X; now let x be set; thus x in FinUnion(B, singleton X) implies x in B proof assume x in FinUnion(B, singleton X); then ex i being Element of X st i in B & x in singleton X.i by Th70; hence thesis by Th68; end; assume A1: x in B; then reconsider x' = x as Element of X by Th14; x in singleton X.x' by Th68; hence x in FinUnion(B, singleton X) by A1,Th70; end; hence FinUnion(B, singleton X) = B by TARSKI:2; end; theorem for Y,Z being set for f being Function of X, Fin Y for g being Function of Fin Y, Fin Z st g.{}.Y = {}.Z & for x,y being Element of Fin Y holds g.(x \/ y) = g.x \/ g.y for B being Element of Fin X holds g.(FinUnion(B,f)) = FinUnion(B,g*f) proof let Y,Z be set; let f be Function of X, Fin Y; let g be Function of Fin Y, Fin Z; assume that A1: g.{}.Y = {}.Z and A2: for x,y being Element of Fin Y holds g.(x \/ y) = g.x \/ g.y; let B be Element of Fin X; A3: FinUnion Z is associative & FinUnion Z is commutative & FinUnion Z is idempotent & FinUnion Z has_a_unity by Th49,Th50,Th51,Th53 ; A4: g.{}.Y = the_unity_wrt FinUnion Z by A1,Th55; now let x,y be Element of Fin Y; thus g.(x \/ y) = g.x \/ g.y by A2 .= FinUnion Z.(g.x,g.y) by Def4; end; hence g.(FinUnion(B,f)) = FinUnion Z $$ (B,g*f) by A3,A4,Th65 .= FinUnion(B,g*f) by Def5; end;

Back to top