:: NORMFORM semantic presentation begin definition let A, B be non empty preBoolean set ; let x, y be Element of [:A,B:]; predx c= y means :: NORMFORM:def 1 ( x `1 c= y `1 & x `2 c= y `2 ); reflexivity for x being Element of [:A,B:] holds ( x `1 c= x `1 & x `2 c= x `2 ) ; funcx \/ y -> Element of [:A,B:] equals :: NORMFORM:def 2 [((x `1) \/ (y `1)),((x `2) \/ (y `2))]; correctness coherence [((x `1) \/ (y `1)),((x `2) \/ (y `2))] is Element of [:A,B:]; ; commutativity for b1, x, y being Element of [:A,B:] st b1 = [((x `1) \/ (y `1)),((x `2) \/ (y `2))] holds b1 = [((y `1) \/ (x `1)),((y `2) \/ (x `2))] ; idempotence for x being Element of [:A,B:] holds x = [((x `1) \/ (x `1)),((x `2) \/ (x `2))] by MCART_1:21; funcx /\ y -> Element of [:A,B:] equals :: NORMFORM:def 3 [((x `1) /\ (y `1)),((x `2) /\ (y `2))]; correctness coherence [((x `1) /\ (y `1)),((x `2) /\ (y `2))] is Element of [:A,B:]; ; commutativity for b1, x, y being Element of [:A,B:] st b1 = [((x `1) /\ (y `1)),((x `2) /\ (y `2))] holds b1 = [((y `1) /\ (x `1)),((y `2) /\ (x `2))] ; idempotence for x being Element of [:A,B:] holds x = [((x `1) /\ (x `1)),((x `2) /\ (x `2))] by MCART_1:21; funcx \ y -> Element of [:A,B:] equals :: NORMFORM:def 4 [((x `1) \ (y `1)),((x `2) \ (y `2))]; correctness coherence [((x `1) \ (y `1)),((x `2) \ (y `2))] is Element of [:A,B:]; ; funcx \+\ y -> Element of [:A,B:] equals :: NORMFORM:def 5 [((x `1) \+\ (y `1)),((x `2) \+\ (y `2))]; correctness coherence [((x `1) \+\ (y `1)),((x `2) \+\ (y `2))] is Element of [:A,B:]; ; commutativity for b1, x, y being Element of [:A,B:] st b1 = [((x `1) \+\ (y `1)),((x `2) \+\ (y `2))] holds b1 = [((y `1) \+\ (x `1)),((y `2) \+\ (x `2))] ; end; :: deftheorem defines c= NORMFORM:def_1_:_ for A, B being non empty preBoolean set for x, y being Element of [:A,B:] holds ( x c= y iff ( x `1 c= y `1 & x `2 c= y `2 ) ); :: deftheorem defines \/ NORMFORM:def_2_:_ for A, B being non empty preBoolean set for x, y being Element of [:A,B:] holds x \/ y = [((x `1) \/ (y `1)),((x `2) \/ (y `2))]; :: deftheorem defines /\ NORMFORM:def_3_:_ for A, B being non empty preBoolean set for x, y being Element of [:A,B:] holds x /\ y = [((x `1) /\ (y `1)),((x `2) /\ (y `2))]; :: deftheorem defines \ NORMFORM:def_4_:_ for A, B being non empty preBoolean set for x, y being Element of [:A,B:] holds x \ y = [((x `1) \ (y `1)),((x `2) \ (y `2))]; :: deftheorem defines \+\ NORMFORM:def_5_:_ for A, B being non empty preBoolean set for x, y being Element of [:A,B:] holds x \+\ y = [((x `1) \+\ (y `1)),((x `2) \+\ (y `2))]; theorem Th1: :: NORMFORM:1 for A, B being non empty preBoolean set for a, b being Element of [:A,B:] st a c= b & b c= a holds a = b proof let A, B be non empty preBoolean set ; ::_thesis: for a, b being Element of [:A,B:] st a c= b & b c= a holds a = b let a, b be Element of [:A,B:]; ::_thesis: ( a c= b & b c= a implies a = b ) assume ( a `1 c= b `1 & a `2 c= b `2 & b `1 c= a `1 & b `2 c= a `2 ) ; :: according to NORMFORM:def_1 ::_thesis: a = b then ( a `1 = b `1 & a `2 = b `2 ) by XBOOLE_0:def_10; hence a = b by DOMAIN_1:2; ::_thesis: verum end; theorem Th2: :: NORMFORM:2 for A, B being non empty preBoolean set for a, b, c being Element of [:A,B:] st a c= b & b c= c holds a c= c proof let A, B be non empty preBoolean set ; ::_thesis: for a, b, c being Element of [:A,B:] st a c= b & b c= c holds a c= c let a, b, c be Element of [:A,B:]; ::_thesis: ( a c= b & b c= c implies a c= c ) assume ( a `1 c= b `1 & a `2 c= b `2 & b `1 c= c `1 & b `2 c= c `2 ) ; :: according to NORMFORM:def_1 ::_thesis: a c= c hence ( a `1 c= c `1 & a `2 c= c `2 ) by XBOOLE_1:1; :: according to NORMFORM:def_1 ::_thesis: verum end; theorem Th3: :: NORMFORM:3 for A, B being non empty preBoolean set for a, b, c being Element of [:A,B:] holds (a \/ b) \/ c = a \/ (b \/ c) proof let A, B be non empty preBoolean set ; ::_thesis: for a, b, c being Element of [:A,B:] holds (a \/ b) \/ c = a \/ (b \/ c) let a, b, c be Element of [:A,B:]; ::_thesis: (a \/ b) \/ c = a \/ (b \/ c) A1: ((a \/ b) \/ c) `2 = ((a \/ b) `2) \/ (c `2) by MCART_1:7 .= ((a `2) \/ (b `2)) \/ (c `2) by MCART_1:7 .= (a `2) \/ ((b `2) \/ (c `2)) by XBOOLE_1:4 .= (a `2) \/ ((b \/ c) `2) by MCART_1:7 .= (a \/ (b \/ c)) `2 by MCART_1:7 ; ((a \/ b) \/ c) `1 = ((a \/ b) `1) \/ (c `1) by MCART_1:7 .= ((a `1) \/ (b `1)) \/ (c `1) by MCART_1:7 .= (a `1) \/ ((b `1) \/ (c `1)) by XBOOLE_1:4 .= (a `1) \/ ((b \/ c) `1) by MCART_1:7 .= (a \/ (b \/ c)) `1 by MCART_1:7 ; hence (a \/ b) \/ c = a \/ (b \/ c) by A1, DOMAIN_1:2; ::_thesis: verum end; theorem :: NORMFORM:4 for A, B being non empty preBoolean set for a, b, c being Element of [:A,B:] holds (a /\ b) /\ c = a /\ (b /\ c) proof let A, B be non empty preBoolean set ; ::_thesis: for a, b, c being Element of [:A,B:] holds (a /\ b) /\ c = a /\ (b /\ c) let a, b, c be Element of [:A,B:]; ::_thesis: (a /\ b) /\ c = a /\ (b /\ c) A1: ((a /\ b) /\ c) `2 = ((a /\ b) `2) /\ (c `2) by MCART_1:7 .= ((a `2) /\ (b `2)) /\ (c `2) by MCART_1:7 .= (a `2) /\ ((b `2) /\ (c `2)) by XBOOLE_1:16 .= (a `2) /\ ((b /\ c) `2) by MCART_1:7 .= (a /\ (b /\ c)) `2 by MCART_1:7 ; ((a /\ b) /\ c) `1 = ((a /\ b) `1) /\ (c `1) by MCART_1:7 .= ((a `1) /\ (b `1)) /\ (c `1) by MCART_1:7 .= (a `1) /\ ((b `1) /\ (c `1)) by XBOOLE_1:16 .= (a `1) /\ ((b /\ c) `1) by MCART_1:7 .= (a /\ (b /\ c)) `1 by MCART_1:7 ; hence (a /\ b) /\ c = a /\ (b /\ c) by A1, DOMAIN_1:2; ::_thesis: verum end; theorem Th5: :: NORMFORM:5 for A, B being non empty preBoolean set for a, b, c being Element of [:A,B:] holds a /\ (b \/ c) = (a /\ b) \/ (a /\ c) proof let A, B be non empty preBoolean set ; ::_thesis: for a, b, c being Element of [:A,B:] holds a /\ (b \/ c) = (a /\ b) \/ (a /\ c) let a, b, c be Element of [:A,B:]; ::_thesis: a /\ (b \/ c) = (a /\ b) \/ (a /\ c) A1: (a /\ (b \/ c)) `2 = (a `2) /\ ((b \/ c) `2) by MCART_1:7 .= (a `2) /\ ((b `2) \/ (c `2)) by MCART_1:7 .= ((a `2) /\ (b `2)) \/ ((a `2) /\ (c `2)) by XBOOLE_1:23 .= ((a `2) /\ (b `2)) \/ ((a /\ c) `2) by MCART_1:7 .= ((a /\ b) `2) \/ ((a /\ c) `2) by MCART_1:7 .= ((a /\ b) \/ (a /\ c)) `2 by MCART_1:7 ; (a /\ (b \/ c)) `1 = (a `1) /\ ((b \/ c) `1) by MCART_1:7 .= (a `1) /\ ((b `1) \/ (c `1)) by MCART_1:7 .= ((a `1) /\ (b `1)) \/ ((a `1) /\ (c `1)) by XBOOLE_1:23 .= ((a `1) /\ (b `1)) \/ ((a /\ c) `1) by MCART_1:7 .= ((a /\ b) `1) \/ ((a /\ c) `1) by MCART_1:7 .= ((a /\ b) \/ (a /\ c)) `1 by MCART_1:7 ; hence a /\ (b \/ c) = (a /\ b) \/ (a /\ c) by A1, DOMAIN_1:2; ::_thesis: verum end; theorem Th6: :: NORMFORM:6 for A, B being non empty preBoolean set for a, b being Element of [:A,B:] holds a \/ (b /\ a) = a proof let A, B be non empty preBoolean set ; ::_thesis: for a, b being Element of [:A,B:] holds a \/ (b /\ a) = a let a, b be Element of [:A,B:]; ::_thesis: a \/ (b /\ a) = a A1: (a \/ (b /\ a)) `2 = (a `2) \/ ((b /\ a) `2) by MCART_1:7 .= (a `2) \/ ((b `2) /\ (a `2)) by MCART_1:7 .= a `2 by XBOOLE_1:22 ; (a \/ (b /\ a)) `1 = (a `1) \/ ((b /\ a) `1) by MCART_1:7 .= (a `1) \/ ((b `1) /\ (a `1)) by MCART_1:7 .= a `1 by XBOOLE_1:22 ; hence a \/ (b /\ a) = a by A1, DOMAIN_1:2; ::_thesis: verum end; theorem Th7: :: NORMFORM:7 for A, B being non empty preBoolean set for a, b being Element of [:A,B:] holds a /\ (b \/ a) = a proof let A, B be non empty preBoolean set ; ::_thesis: for a, b being Element of [:A,B:] holds a /\ (b \/ a) = a let a, b be Element of [:A,B:]; ::_thesis: a /\ (b \/ a) = a thus a /\ (b \/ a) = (a /\ b) \/ (a /\ a) by Th5 .= a by Th6 ; ::_thesis: verum end; theorem :: NORMFORM:8 for A, B being non empty preBoolean set for a, b, c being Element of [:A,B:] holds a \/ (b /\ c) = (a \/ b) /\ (a \/ c) proof let A, B be non empty preBoolean set ; ::_thesis: for a, b, c being Element of [:A,B:] holds a \/ (b /\ c) = (a \/ b) /\ (a \/ c) let a, b, c be Element of [:A,B:]; ::_thesis: a \/ (b /\ c) = (a \/ b) /\ (a \/ c) thus a \/ (b /\ c) = (a \/ (c /\ a)) \/ (c /\ b) by Th6 .= a \/ ((c /\ a) \/ (c /\ b)) by Th3 .= a \/ (c /\ (a \/ b)) by Th5 .= ((a \/ b) /\ a) \/ ((a \/ b) /\ c) by Th7 .= (a \/ b) /\ (a \/ c) by Th5 ; ::_thesis: verum end; theorem Th9: :: NORMFORM:9 for A, B being non empty preBoolean set for a, c, b being Element of [:A,B:] st a c= c & b c= c holds a \/ b c= c proof let A, B be non empty preBoolean set ; ::_thesis: for a, c, b being Element of [:A,B:] st a c= c & b c= c holds a \/ b c= c let a, c, b be Element of [:A,B:]; ::_thesis: ( a c= c & b c= c implies a \/ b c= c ) assume ( a `1 c= c `1 & a `2 c= c `2 & b `1 c= c `1 & b `2 c= c `2 ) ; :: according to NORMFORM:def_1 ::_thesis: a \/ b c= c then ( (a `1) \/ (b `1) c= c `1 & (a `2) \/ (b `2) c= c `2 ) by XBOOLE_1:8; hence ( (a \/ b) `1 c= c `1 & (a \/ b) `2 c= c `2 ) by MCART_1:7; :: according to NORMFORM:def_1 ::_thesis: verum end; theorem Th10: :: NORMFORM:10 for A, B being non empty preBoolean set for a, b being Element of [:A,B:] holds ( a c= a \/ b & b c= a \/ b ) proof let A, B be non empty preBoolean set ; ::_thesis: for a, b being Element of [:A,B:] holds ( a c= a \/ b & b c= a \/ b ) let a, b be Element of [:A,B:]; ::_thesis: ( a c= a \/ b & b c= a \/ b ) ( (a \/ b) `1 = (a `1) \/ (b `1) & (a \/ b) `2 = (a `2) \/ (b `2) ) by MCART_1:7; hence ( a `1 c= (a \/ b) `1 & a `2 c= (a \/ b) `2 & b `1 c= (a \/ b) `1 & b `2 c= (a \/ b) `2 ) by XBOOLE_1:7; :: according to NORMFORM:def_1 ::_thesis: verum end; theorem :: NORMFORM:11 for A, B being non empty preBoolean set for a, b being Element of [:A,B:] st a = a \/ b holds b c= a by Th10; theorem Th12: :: NORMFORM:12 for A, B being non empty preBoolean set for a, b, c being Element of [:A,B:] st a c= b holds ( c \/ a c= c \/ b & a \/ c c= b \/ c ) proof let A, B be non empty preBoolean set ; ::_thesis: for a, b, c being Element of [:A,B:] st a c= b holds ( c \/ a c= c \/ b & a \/ c c= b \/ c ) let a, b, c be Element of [:A,B:]; ::_thesis: ( a c= b implies ( c \/ a c= c \/ b & a \/ c c= b \/ c ) ) assume A1: ( a `1 c= b `1 & a `2 c= b `2 ) ; :: according to NORMFORM:def_1 ::_thesis: ( c \/ a c= c \/ b & a \/ c c= b \/ c ) A2: ( (c \/ b) `1 = (c `1) \/ (b `1) & (c \/ b) `2 = (c `2) \/ (b `2) ) by MCART_1:7; ( (c \/ a) `1 = (c `1) \/ (a `1) & (c \/ a) `2 = (c `2) \/ (a `2) ) by MCART_1:7; hence ( (c \/ a) `1 c= (c \/ b) `1 & (c \/ a) `2 c= (c \/ b) `2 ) by A1, A2, XBOOLE_1:9; :: according to NORMFORM:def_1 ::_thesis: a \/ c c= b \/ c A3: ( (b \/ c) `1 = (b `1) \/ (c `1) & (b \/ c) `2 = (b `2) \/ (c `2) ) by MCART_1:7; ( (a \/ c) `1 = (a `1) \/ (c `1) & (a \/ c) `2 = (a `2) \/ (c `2) ) by MCART_1:7; hence ( (a \/ c) `1 c= (b \/ c) `1 & (a \/ c) `2 c= (b \/ c) `2 ) by A1, A3, XBOOLE_1:9; :: according to NORMFORM:def_1 ::_thesis: verum end; theorem :: NORMFORM:13 for A, B being non empty preBoolean set for a, b being Element of [:A,B:] holds (a \ b) \/ b = a \/ b proof let A, B be non empty preBoolean set ; ::_thesis: for a, b being Element of [:A,B:] holds (a \ b) \/ b = a \/ b let a, b be Element of [:A,B:]; ::_thesis: (a \ b) \/ b = a \/ b A1: (a \ b) `1 = (a `1) \ (b `1) by MCART_1:7; ( ((a `1) \ (b `1)) \/ (b `1) = (a `1) \/ (b `1) & ((a `2) \ (b `2)) \/ (b `2) = (a `2) \/ (b `2) ) by XBOOLE_1:39; hence (a \ b) \/ b = a \/ b by A1, MCART_1:7; ::_thesis: verum end; theorem :: NORMFORM:14 for A, B being non empty preBoolean set for a, b, c being Element of [:A,B:] st a \ b c= c holds a c= b \/ c proof let A, B be non empty preBoolean set ; ::_thesis: for a, b, c being Element of [:A,B:] st a \ b c= c holds a c= b \/ c let a, b, c be Element of [:A,B:]; ::_thesis: ( a \ b c= c implies a c= b \/ c ) assume that A1: (a \ b) `1 c= c `1 and A2: (a \ b) `2 c= c `2 ; :: according to NORMFORM:def_1 ::_thesis: a c= b \/ c (a `2) \ (b `2) c= c `2 by A2, MCART_1:7; then A3: a `2 c= (b `2) \/ (c `2) by XBOOLE_1:44; (a `1) \ (b `1) c= c `1 by A1, MCART_1:7; then a `1 c= (b `1) \/ (c `1) by XBOOLE_1:44; hence ( a `1 c= (b \/ c) `1 & a `2 c= (b \/ c) `2 ) by A3, MCART_1:7; :: according to NORMFORM:def_1 ::_thesis: verum end; theorem :: NORMFORM:15 for A, B being non empty preBoolean set for a, b, c being Element of [:A,B:] st a c= b \/ c holds a \ c c= b proof let A, B be non empty preBoolean set ; ::_thesis: for a, b, c being Element of [:A,B:] st a c= b \/ c holds a \ c c= b let a, b, c be Element of [:A,B:]; ::_thesis: ( a c= b \/ c implies a \ c c= b ) A1: ( (b \/ c) `1 = (b `1) \/ (c `1) & (b \/ c) `2 = (b `2) \/ (c `2) ) by MCART_1:7; A2: ( (a \ c) `1 = (a `1) \ (c `1) & (a \ c) `2 = (a `2) \ (c `2) ) by MCART_1:7; assume ( a `1 c= (b \/ c) `1 & a `2 c= (b \/ c) `2 ) ; :: according to NORMFORM:def_1 ::_thesis: a \ c c= b hence ( (a \ c) `1 c= b `1 & (a \ c) `2 c= b `2 ) by A1, A2, XBOOLE_1:43; :: according to NORMFORM:def_1 ::_thesis: verum end; definition let A be set ; func FinPairUnion A -> BinOp of [:(Fin A),(Fin A):] means :Def6: :: NORMFORM:def 6 for x, y being Element of [:(Fin A),(Fin A):] holds it . (x,y) = x \/ y; existence ex b1 being BinOp of [:(Fin A),(Fin A):] st for x, y being Element of [:(Fin A),(Fin A):] holds b1 . (x,y) = x \/ y proof deffunc H1( Element of [:(Fin A),(Fin A):], Element of [:(Fin A),(Fin A):]) -> Element of [:(Fin A),(Fin A):] = $1 \/ $2; ex IT being BinOp of [:(Fin A),(Fin A):] st for x, y being Element of [:(Fin A),(Fin A):] holds IT . (x,y) = H1(x,y) from BINOP_1:sch_4(); hence ex b1 being BinOp of [:(Fin A),(Fin A):] st for x, y being Element of [:(Fin A),(Fin A):] holds b1 . (x,y) = x \/ y ; ::_thesis: verum end; uniqueness for b1, b2 being BinOp of [:(Fin A),(Fin A):] st ( for x, y being Element of [:(Fin A),(Fin A):] holds b1 . (x,y) = x \/ y ) & ( for x, y being Element of [:(Fin A),(Fin A):] holds b2 . (x,y) = x \/ y ) holds b1 = b2 proof let IT, IT9 be BinOp of [:(Fin A),(Fin A):]; ::_thesis: ( ( for x, y being Element of [:(Fin A),(Fin A):] holds IT . (x,y) = x \/ y ) & ( for x, y being Element of [:(Fin A),(Fin A):] holds IT9 . (x,y) = x \/ y ) implies IT = IT9 ) assume that A1: for x, y being Element of [:(Fin A),(Fin A):] holds IT . (x,y) = x \/ y and A2: for x, y being Element of [:(Fin A),(Fin A):] holds IT9 . (x,y) = x \/ y ; ::_thesis: IT = IT9 now__::_thesis:_for_x,_y_being_Element_of_[:(Fin_A),(Fin_A):]_holds_IT_._(x,y)_=_IT9_._(x,y) let x, y be Element of [:(Fin A),(Fin A):]; ::_thesis: IT . (x,y) = IT9 . (x,y) thus IT . (x,y) = x \/ y by A1 .= IT9 . (x,y) by A2 ; ::_thesis: verum end; hence IT = IT9 by BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def6 defines FinPairUnion NORMFORM:def_6_:_ for A being set for b2 being BinOp of [:(Fin A),(Fin A):] holds ( b2 = FinPairUnion A iff for x, y being Element of [:(Fin A),(Fin A):] holds b2 . (x,y) = x \/ y ); definition let X be non empty set ; let A be set ; let B be Element of Fin X; let f be Function of X,[:(Fin A),(Fin A):]; func FinPairUnion (B,f) -> Element of [:(Fin A),(Fin A):] equals :: NORMFORM:def 7 (FinPairUnion A) $$ (B,f); correctness coherence (FinPairUnion A) $$ (B,f) is Element of [:(Fin A),(Fin A):]; ; end; :: deftheorem defines FinPairUnion NORMFORM:def_7_:_ for X being non empty set for A being set for B being Element of Fin X for f being Function of X,[:(Fin A),(Fin A):] holds FinPairUnion (B,f) = (FinPairUnion A) $$ (B,f); Lm1: for A being set holds FinPairUnion A is idempotent proof let A be set ; ::_thesis: FinPairUnion A is idempotent let a be Element of [:(Fin A),(Fin A):]; :: according to BINOP_1:def_4 ::_thesis: (FinPairUnion A) . (a,a) = a thus (FinPairUnion A) . (a,a) = a \/ a by Def6 .= a ; ::_thesis: verum end; Lm2: for A being set holds FinPairUnion A is commutative proof let A be set ; ::_thesis: FinPairUnion A is commutative let a, b be Element of [:(Fin A),(Fin A):]; :: according to BINOP_1:def_2 ::_thesis: (FinPairUnion A) . (a,b) = (FinPairUnion A) . (b,a) thus (FinPairUnion A) . (a,b) = b \/ a by Def6 .= (FinPairUnion A) . (b,a) by Def6 ; ::_thesis: verum end; Lm3: for A being set holds FinPairUnion A is associative proof let A be set ; ::_thesis: FinPairUnion A is associative let a, b, c be Element of [:(Fin A),(Fin A):]; :: according to BINOP_1:def_3 ::_thesis: (FinPairUnion A) . (a,((FinPairUnion A) . (b,c))) = (FinPairUnion A) . (((FinPairUnion A) . (a,b)),c) thus (FinPairUnion A) . (a,((FinPairUnion A) . (b,c))) = a \/ ((FinPairUnion A) . (b,c)) by Def6 .= a \/ (b \/ c) by Def6 .= (a \/ b) \/ c by Th3 .= ((FinPairUnion A) . (a,b)) \/ c by Def6 .= (FinPairUnion A) . (((FinPairUnion A) . (a,b)),c) by Def6 ; ::_thesis: verum end; registration let A be set ; cluster FinPairUnion A -> commutative associative idempotent ; coherence ( FinPairUnion A is commutative & FinPairUnion A is idempotent & FinPairUnion A is associative ) by Lm1, Lm2, Lm3; end; theorem :: NORMFORM:16 for A being set for X being non empty set for f being Function of X,[:(Fin A),(Fin A):] for B being Element of Fin X for x being Element of X st x in B holds f . x c= FinPairUnion (B,f) proof let A be set ; ::_thesis: for X being non empty set for f being Function of X,[:(Fin A),(Fin A):] for B being Element of Fin X for x being Element of X st x in B holds f . x c= FinPairUnion (B,f) let X be non empty set ; ::_thesis: for f being Function of X,[:(Fin A),(Fin A):] for B being Element of Fin X for x being Element of X st x in B holds f . x c= FinPairUnion (B,f) let f be Function of X,[:(Fin A),(Fin A):]; ::_thesis: for B being Element of Fin X for x being Element of X st x in B holds f . x c= FinPairUnion (B,f) let B be Element of Fin X; ::_thesis: for x being Element of X st x in B holds f . x c= FinPairUnion (B,f) let x be Element of X; ::_thesis: ( x in B implies f . x c= FinPairUnion (B,f) ) assume A1: x in B ; ::_thesis: f . x c= FinPairUnion (B,f) then (FinPairUnion A) $$ (B,f) = (FinPairUnion A) $$ ((B \/ {.x.}),f) by ZFMISC_1:40 .= (FinPairUnion A) . (((FinPairUnion A) $$ (B,f)),(f . x)) by A1, SETWISEO:20 .= ((FinPairUnion A) $$ (B,f)) \/ (f . x) by Def6 ; hence f . x c= FinPairUnion (B,f) by Th10; ::_thesis: verum end; theorem Th17: :: NORMFORM:17 for A being set holds [({}. A),({}. A)] is_a_unity_wrt FinPairUnion A proof let A be set ; ::_thesis: [({}. A),({}. A)] is_a_unity_wrt FinPairUnion A now__::_thesis:_for_x_being_Element_of_[:(Fin_A),(Fin_A):]_holds_(FinPairUnion_A)_._([({}._A),({}._A)],x)_=_x let x be Element of [:(Fin A),(Fin A):]; ::_thesis: (FinPairUnion A) . ([({}. A),({}. A)],x) = x thus (FinPairUnion A) . ([({}. A),({}. A)],x) = [({}. A),({}. A)] \/ x by Def6 .= x by MCART_1:21 ; ::_thesis: verum end; hence [({}. A),({}. A)] is_a_unity_wrt FinPairUnion A by BINOP_1:4; ::_thesis: verum end; theorem Th18: :: NORMFORM:18 for A being set holds FinPairUnion A is having_a_unity proof let A be set ; ::_thesis: FinPairUnion A is having_a_unity [({}. A),({}. A)] is_a_unity_wrt FinPairUnion A by Th17; hence FinPairUnion A is having_a_unity by SETWISEO:def_2; ::_thesis: verum end; theorem Th19: :: NORMFORM:19 for A being set holds the_unity_wrt (FinPairUnion A) = [({}. A),({}. A)] proof let A be set ; ::_thesis: the_unity_wrt (FinPairUnion A) = [({}. A),({}. A)] [({}. A),({}. A)] is_a_unity_wrt FinPairUnion A by Th17; hence the_unity_wrt (FinPairUnion A) = [({}. A),({}. A)] by BINOP_1:def_8; ::_thesis: verum end; theorem Th20: :: NORMFORM:20 for A being set for x being Element of [:(Fin A),(Fin A):] holds the_unity_wrt (FinPairUnion A) c= x proof let A be set ; ::_thesis: for x being Element of [:(Fin A),(Fin A):] holds the_unity_wrt (FinPairUnion A) c= x let x be Element of [:(Fin A),(Fin A):]; ::_thesis: the_unity_wrt (FinPairUnion A) c= x [({}. A),({}. A)] is_a_unity_wrt FinPairUnion A by Th17; then the_unity_wrt (FinPairUnion A) = [{},{}] by BINOP_1:def_8; then ( (the_unity_wrt (FinPairUnion A)) `1 = {} & (the_unity_wrt (FinPairUnion A)) `2 = {} ) by MCART_1:7; hence ( (the_unity_wrt (FinPairUnion A)) `1 c= x `1 & (the_unity_wrt (FinPairUnion A)) `2 c= x `2 ) by XBOOLE_1:2; :: according to NORMFORM:def_1 ::_thesis: verum end; theorem :: NORMFORM:21 for A being set for X being non empty set for f being Function of X,[:(Fin A),(Fin A):] for B being Element of Fin X for c being Element of [:(Fin A),(Fin A):] st ( for x being Element of X st x in B holds f . x c= c ) holds FinPairUnion (B,f) c= c proof let A be set ; ::_thesis: for X being non empty set for f being Function of X,[:(Fin A),(Fin A):] for B being Element of Fin X for c being Element of [:(Fin A),(Fin A):] st ( for x being Element of X st x in B holds f . x c= c ) holds FinPairUnion (B,f) c= c let X be non empty set ; ::_thesis: for f being Function of X,[:(Fin A),(Fin A):] for B being Element of Fin X for c being Element of [:(Fin A),(Fin A):] st ( for x being Element of X st x in B holds f . x c= c ) holds FinPairUnion (B,f) c= c let f be Function of X,[:(Fin A),(Fin A):]; ::_thesis: for B being Element of Fin X for c being Element of [:(Fin A),(Fin A):] st ( for x being Element of X st x in B holds f . x c= c ) holds FinPairUnion (B,f) c= c let B be Element of Fin X; ::_thesis: for c being Element of [:(Fin A),(Fin A):] st ( for x being Element of X st x in B holds f . x c= c ) holds FinPairUnion (B,f) c= c let c be Element of [:(Fin A),(Fin A):]; ::_thesis: ( ( for x being Element of X st x in B holds f . x c= c ) implies FinPairUnion (B,f) c= c ) defpred S1[ Element of Fin X] means ( $1 c= B implies (FinPairUnion A) $$ ($1,f) c= c ); assume A1: for x being Element of X st x in B holds f . x c= c ; ::_thesis: FinPairUnion (B,f) c= c A2: now__::_thesis:_for_C_being_Element_of_Fin_X for_b_being_Element_of_X_st_S1[C]_holds_ S1[C_\/_{.b.}] let C be Element of Fin X; ::_thesis: for b being Element of X st S1[C] holds S1[C \/ {.b.}] let b be Element of X; ::_thesis: ( S1[C] implies S1[C \/ {.b.}] ) assume A3: S1[C] ; ::_thesis: S1[C \/ {.b.}] now__::_thesis:_(_C_\/_{b}_c=_B_implies_(FinPairUnion_A)_$$_((C_\/_{.b.}),f)_c=_c_) assume A4: C \/ {b} c= B ; ::_thesis: (FinPairUnion A) $$ ((C \/ {.b.}),f) c= c then {b} c= B by XBOOLE_1:11; then b in B by ZFMISC_1:31; then A5: f . b c= c by A1; (FinPairUnion A) $$ ((C \/ {.b.}),f) = (FinPairUnion A) . (((FinPairUnion A) $$ (C,f)),(f . b)) by Th18, SETWISEO:32 .= ((FinPairUnion A) $$ (C,f)) \/ (f . b) by Def6 ; hence (FinPairUnion A) $$ ((C \/ {.b.}),f) c= c by A3, A4, A5, Th9, XBOOLE_1:11; ::_thesis: verum end; hence S1[C \/ {.b.}] ; ::_thesis: verum end; A6: S1[ {}. X] proof assume {}. X c= B ; ::_thesis: (FinPairUnion A) $$ (({}. X),f) c= c (FinPairUnion A) $$ (({}. X),f) = the_unity_wrt (FinPairUnion A) by Th18, SETWISEO:31; hence (FinPairUnion A) $$ (({}. X),f) c= c by Th20; ::_thesis: verum end; for C being Element of Fin X holds S1[C] from SETWISEO:sch_4(A6, A2); hence FinPairUnion (B,f) c= c ; ::_thesis: verum end; theorem :: NORMFORM:22 for A being set for X being non empty set for B being Element of Fin X for f, g being Function of X,[:(Fin A),(Fin A):] st f | B = g | B holds FinPairUnion (B,f) = FinPairUnion (B,g) proof let A be set ; ::_thesis: for X being non empty set for B being Element of Fin X for f, g being Function of X,[:(Fin A),(Fin A):] st f | B = g | B holds FinPairUnion (B,f) = FinPairUnion (B,g) let X be non empty set ; ::_thesis: for B being Element of Fin X for f, g being Function of X,[:(Fin A),(Fin A):] st f | B = g | B holds FinPairUnion (B,f) = FinPairUnion (B,g) let B be Element of Fin X; ::_thesis: for f, g being Function of X,[:(Fin A),(Fin A):] st f | B = g | B holds FinPairUnion (B,f) = FinPairUnion (B,g) let f, g be Function of X,[:(Fin A),(Fin A):]; ::_thesis: ( f | B = g | B implies FinPairUnion (B,f) = FinPairUnion (B,g) ) set J = FinPairUnion A; A1: [({}. A),({}. A)] = the_unity_wrt (FinPairUnion A) by Th19; assume A2: f | B = g | B ; ::_thesis: FinPairUnion (B,f) = FinPairUnion (B,g) now__::_thesis:_FinPairUnion_(B,f)_=_FinPairUnion_(B,g) percases ( B = {} or B <> {} ) ; supposeA3: B = {} ; ::_thesis: FinPairUnion (B,f) = FinPairUnion (B,g) hence FinPairUnion (B,f) = (FinPairUnion A) $$ (({}. X),f) .= [({}. A),({}. A)] by A1, Th18, SETWISEO:31 .= (FinPairUnion A) $$ (({}. X),g) by A1, Th18, SETWISEO:31 .= FinPairUnion (B,g) by A3 ; ::_thesis: verum end; supposeA4: B <> {} ; ::_thesis: FinPairUnion (B,f) = FinPairUnion (B,g) f .: B = g .: B by A2, RELAT_1:166; hence FinPairUnion (B,f) = FinPairUnion (B,g) by A4, SETWISEO:26; ::_thesis: verum end; end; end; hence FinPairUnion (B,f) = FinPairUnion (B,g) ; ::_thesis: verum end; definition let X be set ; func DISJOINT_PAIRS X -> Subset of [:(Fin X),(Fin X):] equals :: NORMFORM:def 8 { a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } ; coherence { a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } is Subset of [:(Fin X),(Fin X):] proof set D = { a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } ; { a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } c= [:(Fin X),(Fin X):] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } or x in [:(Fin X),(Fin X):] ) assume x in { a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } ; ::_thesis: x in [:(Fin X),(Fin X):] then ex a being Element of [:(Fin X),(Fin X):] st ( x = a & a `1 misses a `2 ) ; hence x in [:(Fin X),(Fin X):] ; ::_thesis: verum end; hence { a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } is Subset of [:(Fin X),(Fin X):] ; ::_thesis: verum end; end; :: deftheorem defines DISJOINT_PAIRS NORMFORM:def_8_:_ for X being set holds DISJOINT_PAIRS X = { a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } ; registration let X be set ; cluster DISJOINT_PAIRS X -> non empty ; coherence not DISJOINT_PAIRS X is empty proof {} is Element of Fin X by FINSUB_1:7; then reconsider b = [{},{}] as Element of [:(Fin X),(Fin X):] by ZFMISC_1:def_2; b `1 = {} by MCART_1:7; then b `1 misses b `2 by XBOOLE_1:65; then b in { a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } ; hence not DISJOINT_PAIRS X is empty ; ::_thesis: verum end; end; theorem Th23: :: NORMFORM:23 for X being set for y being Element of [:(Fin X),(Fin X):] holds ( y in DISJOINT_PAIRS X iff y `1 misses y `2 ) proof let X be set ; ::_thesis: for y being Element of [:(Fin X),(Fin X):] holds ( y in DISJOINT_PAIRS X iff y `1 misses y `2 ) let y be Element of [:(Fin X),(Fin X):]; ::_thesis: ( y in DISJOINT_PAIRS X iff y `1 misses y `2 ) ( y in DISJOINT_PAIRS X iff ex a being Element of [:(Fin X),(Fin X):] st ( y = a & a `1 misses a `2 ) ) ; hence ( y in DISJOINT_PAIRS X iff y `1 misses y `2 ) ; ::_thesis: verum end; theorem :: NORMFORM:24 for X being set for y, x being Element of [:(Fin X),(Fin X):] st y in DISJOINT_PAIRS X & x in DISJOINT_PAIRS X holds ( y \/ x in DISJOINT_PAIRS X iff ((y `1) /\ (x `2)) \/ ((x `1) /\ (y `2)) = {} ) proof let X be set ; ::_thesis: for y, x being Element of [:(Fin X),(Fin X):] st y in DISJOINT_PAIRS X & x in DISJOINT_PAIRS X holds ( y \/ x in DISJOINT_PAIRS X iff ((y `1) /\ (x `2)) \/ ((x `1) /\ (y `2)) = {} ) let y, x be Element of [:(Fin X),(Fin X):]; ::_thesis: ( y in DISJOINT_PAIRS X & x in DISJOINT_PAIRS X implies ( y \/ x in DISJOINT_PAIRS X iff ((y `1) /\ (x `2)) \/ ((x `1) /\ (y `2)) = {} ) ) assume that A1: y in DISJOINT_PAIRS X and A2: x in DISJOINT_PAIRS X ; ::_thesis: ( y \/ x in DISJOINT_PAIRS X iff ((y `1) /\ (x `2)) \/ ((x `1) /\ (y `2)) = {} ) A3: ( ((y `1) \/ (x `1)) /\ ((y `2) \/ (x `2)) = (((y `1) \/ (x `1)) /\ (y `2)) \/ (((y `1) \/ (x `1)) /\ (x `2)) & ((y `1) \/ (x `1)) /\ (y `2) = ((y `1) /\ (y `2)) \/ ((x `1) /\ (y `2)) ) by XBOOLE_1:23; x `1 misses x `2 by A2, Th23; then A4: (x `1) /\ (x `2) = {} by XBOOLE_0:def_7; y `1 misses y `2 by A1, Th23; then A5: (y `1) /\ (y `2) = {} by XBOOLE_0:def_7; A6: ((y `1) \/ (x `1)) /\ (x `2) = ((y `1) /\ (x `2)) \/ ((x `1) /\ (x `2)) by XBOOLE_1:23; A7: ( (y \/ x) `1 = (y `1) \/ (x `1) & (y \/ x) `2 = (y `2) \/ (x `2) ) by MCART_1:7; hereby ::_thesis: ( ((y `1) /\ (x `2)) \/ ((x `1) /\ (y `2)) = {} implies y \/ x in DISJOINT_PAIRS X ) assume y \/ x in DISJOINT_PAIRS X ; ::_thesis: ((y `1) /\ (x `2)) \/ ((x `1) /\ (y `2)) = {} then (y \/ x) `1 misses (y \/ x) `2 by Th23; hence ((y `1) /\ (x `2)) \/ ((x `1) /\ (y `2)) = {} by A5, A4, A7, A3, A6, XBOOLE_0:def_7; ::_thesis: verum end; assume ((y `1) /\ (x `2)) \/ ((x `1) /\ (y `2)) = {} ; ::_thesis: y \/ x in DISJOINT_PAIRS X then (y \/ x) `1 misses (y \/ x) `2 by A5, A4, A7, A3, A6, XBOOLE_0:def_7; hence y \/ x in DISJOINT_PAIRS X ; ::_thesis: verum end; theorem :: NORMFORM:25 for X being set for a being Element of DISJOINT_PAIRS X holds a `1 misses a `2 by Th23; theorem Th26: :: NORMFORM:26 for X being set for x being Element of [:(Fin X),(Fin X):] for b being Element of DISJOINT_PAIRS X st x c= b holds x is Element of DISJOINT_PAIRS X proof let X be set ; ::_thesis: for x being Element of [:(Fin X),(Fin X):] for b being Element of DISJOINT_PAIRS X st x c= b holds x is Element of DISJOINT_PAIRS X let x be Element of [:(Fin X),(Fin X):]; ::_thesis: for b being Element of DISJOINT_PAIRS X st x c= b holds x is Element of DISJOINT_PAIRS X let b be Element of DISJOINT_PAIRS X; ::_thesis: ( x c= b implies x is Element of DISJOINT_PAIRS X ) assume A1: ( x `1 c= b `1 & x `2 c= b `2 ) ; :: according to NORMFORM:def_1 ::_thesis: x is Element of DISJOINT_PAIRS X b `1 misses b `2 by Th23; then x `1 misses x `2 by A1, XBOOLE_1:64; hence x is Element of DISJOINT_PAIRS X by Th23; ::_thesis: verum end; theorem Th27: :: NORMFORM:27 for X being set for a being Element of DISJOINT_PAIRS X for x being set holds ( not x in a `1 or not x in a `2 ) proof let X be set ; ::_thesis: for a being Element of DISJOINT_PAIRS X for x being set holds ( not x in a `1 or not x in a `2 ) let a be Element of DISJOINT_PAIRS X; ::_thesis: for x being set holds ( not x in a `1 or not x in a `2 ) a `1 misses a `2 by Th23; hence for x being set holds ( not x in a `1 or not x in a `2 ) by XBOOLE_0:3; ::_thesis: verum end; theorem :: NORMFORM:28 for X being set for a, b being Element of DISJOINT_PAIRS X st not a \/ b in DISJOINT_PAIRS X holds ex p being Element of X st ( ( p in a `1 & p in b `2 ) or ( p in b `1 & p in a `2 ) ) proof let X be set ; ::_thesis: for a, b being Element of DISJOINT_PAIRS X st not a \/ b in DISJOINT_PAIRS X holds ex p being Element of X st ( ( p in a `1 & p in b `2 ) or ( p in b `1 & p in a `2 ) ) let a, b be Element of DISJOINT_PAIRS X; ::_thesis: ( not a \/ b in DISJOINT_PAIRS X implies ex p being Element of X st ( ( p in a `1 & p in b `2 ) or ( p in b `1 & p in a `2 ) ) ) set p = the Element of ((a \/ b) `1) /\ ((a \/ b) `2); assume not a \/ b in DISJOINT_PAIRS X ; ::_thesis: ex p being Element of X st ( ( p in a `1 & p in b `2 ) or ( p in b `1 & p in a `2 ) ) then (a \/ b) `1 meets (a \/ b) `2 ; then A1: ((a \/ b) `1) /\ ((a \/ b) `2) <> {} by XBOOLE_0:def_7; ((a \/ b) `1) /\ ((a \/ b) `2) is Subset of X by FINSUB_1:17; then reconsider p = the Element of ((a \/ b) `1) /\ ((a \/ b) `2) as Element of X by A1, TARSKI:def_3; p in (a \/ b) `2 by A1, XBOOLE_0:def_4; then p in (a `2) \/ (b `2) by MCART_1:7; then A2: ( p in b `2 or p in a `2 ) by XBOOLE_0:def_3; take p ; ::_thesis: ( ( p in a `1 & p in b `2 ) or ( p in b `1 & p in a `2 ) ) p in (a \/ b) `1 by A1, XBOOLE_0:def_4; then p in (a `1) \/ (b `1) by MCART_1:7; then ( p in a `1 or p in b `1 ) by XBOOLE_0:def_3; hence ( ( p in a `1 & p in b `2 ) or ( p in b `1 & p in a `2 ) ) by A2, Th27; ::_thesis: verum end; theorem :: NORMFORM:29 for X being set for x being Element of [:(Fin X),(Fin X):] st x `1 misses x `2 holds x is Element of DISJOINT_PAIRS X by Th23; theorem :: NORMFORM:30 for X being set for a being Element of DISJOINT_PAIRS X for V, W being set st V c= a `1 & W c= a `2 holds [V,W] is Element of DISJOINT_PAIRS X proof let X be set ; ::_thesis: for a being Element of DISJOINT_PAIRS X for V, W being set st V c= a `1 & W c= a `2 holds [V,W] is Element of DISJOINT_PAIRS X let a be Element of DISJOINT_PAIRS X; ::_thesis: for V, W being set st V c= a `1 & W c= a `2 holds [V,W] is Element of DISJOINT_PAIRS X let V, W be set ; ::_thesis: ( V c= a `1 & W c= a `2 implies [V,W] is Element of DISJOINT_PAIRS X ) A1: [V,W] `2 = W ; assume A2: ( V c= a `1 & W c= a `2 ) ; ::_thesis: [V,W] is Element of DISJOINT_PAIRS X then ( V is Element of Fin X & W is Element of Fin X ) by SETWISEO:11; then reconsider x = [V,W] as Element of [:(Fin X),(Fin X):] by ZFMISC_1:def_2; ( a `1 misses a `2 & [V,W] `1 = V ) by Th23; then x `1 misses x `2 by A1, A2, XBOOLE_1:64; hence [V,W] is Element of DISJOINT_PAIRS X by Th23; ::_thesis: verum end; Lm4: for A being set holds {} in { B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds a = b } proof let A be set ; ::_thesis: {} in { B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds a = b } ( {} is Element of Fin (DISJOINT_PAIRS A) & ( for a, b being Element of DISJOINT_PAIRS A st a in {} & b in {} & a c= b holds a = b ) ) by FINSUB_1:7; hence {} in { B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds a = b } ; ::_thesis: verum end; definition let A be set ; func Normal_forms_on A -> Subset of (Fin (DISJOINT_PAIRS A)) equals :: NORMFORM:def 9 { B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds a = b } ; coherence { B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds a = b } is Subset of (Fin (DISJOINT_PAIRS A)) proof set IT = { B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds a = b } ; { B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds a = b } c= Fin (DISJOINT_PAIRS A) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds a = b } or x in Fin (DISJOINT_PAIRS A) ) assume x in { B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds a = b } ; ::_thesis: x in Fin (DISJOINT_PAIRS A) then ex B being Element of Fin (DISJOINT_PAIRS A) st ( x = B & ( for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds a = b ) ) ; hence x in Fin (DISJOINT_PAIRS A) ; ::_thesis: verum end; hence { B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds a = b } is Subset of (Fin (DISJOINT_PAIRS A)) ; ::_thesis: verum end; end; :: deftheorem defines Normal_forms_on NORMFORM:def_9_:_ for A being set holds Normal_forms_on A = { B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds a = b } ; registration let A be set ; cluster Normal_forms_on A -> non empty ; coherence not Normal_forms_on A is empty by Lm4; end; theorem :: NORMFORM:31 for A being set holds {} in Normal_forms_on A by Lm4; theorem Th32: :: NORMFORM:32 for A being set for a, b being Element of DISJOINT_PAIRS A for B being Element of Fin (DISJOINT_PAIRS A) st B in Normal_forms_on A & a in B & b in B & a c= b holds a = b proof let A be set ; ::_thesis: for a, b being Element of DISJOINT_PAIRS A for B being Element of Fin (DISJOINT_PAIRS A) st B in Normal_forms_on A & a in B & b in B & a c= b holds a = b let a, b be Element of DISJOINT_PAIRS A; ::_thesis: for B being Element of Fin (DISJOINT_PAIRS A) st B in Normal_forms_on A & a in B & b in B & a c= b holds a = b let B be Element of Fin (DISJOINT_PAIRS A); ::_thesis: ( B in Normal_forms_on A & a in B & b in B & a c= b implies a = b ) assume B in Normal_forms_on A ; ::_thesis: ( not a in B or not b in B or not a c= b or a = b ) then ex C being Element of Fin (DISJOINT_PAIRS A) st ( B = C & ( for a, b being Element of DISJOINT_PAIRS A st a in C & b in C & a c= b holds a = b ) ) ; hence ( not a in B or not b in B or not a c= b or a = b ) ; ::_thesis: verum end; theorem Th33: :: NORMFORM:33 for A being set for B being Element of Fin (DISJOINT_PAIRS A) st ( for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds a = b ) holds B in Normal_forms_on A ; definition let A be set ; let B be Element of Fin (DISJOINT_PAIRS A); func mi B -> Element of Normal_forms_on A equals :: NORMFORM:def 10 { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds ( ( s in B & s c= t ) iff s = t ) } ; coherence { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds ( ( s in B & s c= t ) iff s = t ) } is Element of Normal_forms_on A proof set M = { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds ( ( s in B & s c= t ) iff s = t ) } ; now__::_thesis:_for_x_being_set_st_x_in__{__t_where_t_is_Element_of_DISJOINT_PAIRS_A_:_for_s_being_Element_of_DISJOINT_PAIRS_A_holds_ (_(_s_in_B_&_s_c=_t_)_iff_s_=_t_)__}__holds_ x_in_B let x be set ; ::_thesis: ( x in { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds ( ( s in B & s c= t ) iff s = t ) } implies x in B ) assume x in { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds ( ( s in B & s c= t ) iff s = t ) } ; ::_thesis: x in B then ex t being Element of DISJOINT_PAIRS A st ( x = t & ( for s being Element of DISJOINT_PAIRS A holds ( ( s in B & s c= t ) iff s = t ) ) ) ; hence x in B ; ::_thesis: verum end; then A1: { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds ( ( s in B & s c= t ) iff s = t ) } c= B by TARSKI:def_3; then A2: { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds ( ( s in B & s c= t ) iff s = t ) } is finite by FINSET_1:1; B c= DISJOINT_PAIRS A by FINSUB_1:def_5; then { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds ( ( s in B & s c= t ) iff s = t ) } c= DISJOINT_PAIRS A by A1, XBOOLE_1:1; then reconsider M9 = { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds ( ( s in B & s c= t ) iff s = t ) } as Element of Fin (DISJOINT_PAIRS A) by A2, FINSUB_1:def_5; now__::_thesis:_for_c,_d_being_Element_of_DISJOINT_PAIRS_A_st_c_in__{__t_where_t_is_Element_of_DISJOINT_PAIRS_A_:_for_s_being_Element_of_DISJOINT_PAIRS_A_holds_ (_(_s_in_B_&_s_c=_t_)_iff_s_=_t_)__}__&_d_in__{__t_where_t_is_Element_of_DISJOINT_PAIRS_A_:_for_s_being_Element_of_DISJOINT_PAIRS_A_holds_ (_(_s_in_B_&_s_c=_t_)_iff_s_=_t_)__}__&_c_c=_d_holds_ c_=_d let c, d be Element of DISJOINT_PAIRS A; ::_thesis: ( c in { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds ( ( s in B & s c= t ) iff s = t ) } & d in { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds ( ( s in B & s c= t ) iff s = t ) } & c c= d implies c = d ) assume c in { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds ( ( s in B & s c= t ) iff s = t ) } ; ::_thesis: ( d in { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds ( ( s in B & s c= t ) iff s = t ) } & c c= d implies c = d ) then ex t being Element of DISJOINT_PAIRS A st ( c = t & ( for s being Element of DISJOINT_PAIRS A holds ( ( s in B & s c= t ) iff s = t ) ) ) ; then A3: c in B ; assume d in { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds ( ( s in B & s c= t ) iff s = t ) } ; ::_thesis: ( c c= d implies c = d ) then ex t being Element of DISJOINT_PAIRS A st ( d = t & ( for s being Element of DISJOINT_PAIRS A holds ( ( s in B & s c= t ) iff s = t ) ) ) ; hence ( c c= d implies c = d ) by A3; ::_thesis: verum end; then M9 is Element of Normal_forms_on A by Th33; hence { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds ( ( s in B & s c= t ) iff s = t ) } is Element of Normal_forms_on A ; ::_thesis: verum end; correctness ; let C be Element of Fin (DISJOINT_PAIRS A); funcB ^ C -> Element of Fin (DISJOINT_PAIRS A) equals :: NORMFORM:def 11 (DISJOINT_PAIRS A) /\ { (s \/ t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } ; coherence (DISJOINT_PAIRS A) /\ { (s \/ t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } is Element of Fin (DISJOINT_PAIRS A) proof deffunc H1( Element of DISJOINT_PAIRS A, Element of DISJOINT_PAIRS A) -> Element of [:(Fin A),(Fin A):] = $1 \/ $2; set M = (DISJOINT_PAIRS A) /\ { H1(s,t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } ; A4: C is finite ; A5: B is finite ; { H1(s,t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } is finite from FRAENKEL:sch_22(A5, A4); then ( (DISJOINT_PAIRS A) /\ { H1(s,t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } c= DISJOINT_PAIRS A & (DISJOINT_PAIRS A) /\ { H1(s,t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } is finite ) by FINSET_1:1, XBOOLE_1:17; hence (DISJOINT_PAIRS A) /\ { (s \/ t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } is Element of Fin (DISJOINT_PAIRS A) by FINSUB_1:def_5; ::_thesis: verum end; correctness ; end; :: deftheorem defines mi NORMFORM:def_10_:_ for A being set for B being Element of Fin (DISJOINT_PAIRS A) holds mi B = { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds ( ( s in B & s c= t ) iff s = t ) } ; :: deftheorem defines ^ NORMFORM:def_11_:_ for A being set for B, C being Element of Fin (DISJOINT_PAIRS A) holds B ^ C = (DISJOINT_PAIRS A) /\ { (s \/ t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } ; theorem Th34: :: NORMFORM:34 for A being set for x being Element of [:(Fin A),(Fin A):] for B, C being Element of Fin (DISJOINT_PAIRS A) st x in B ^ C holds ex b, c being Element of DISJOINT_PAIRS A st ( b in B & c in C & x = b \/ c ) proof let A be set ; ::_thesis: for x being Element of [:(Fin A),(Fin A):] for B, C being Element of Fin (DISJOINT_PAIRS A) st x in B ^ C holds ex b, c being Element of DISJOINT_PAIRS A st ( b in B & c in C & x = b \/ c ) let x be Element of [:(Fin A),(Fin A):]; ::_thesis: for B, C being Element of Fin (DISJOINT_PAIRS A) st x in B ^ C holds ex b, c being Element of DISJOINT_PAIRS A st ( b in B & c in C & x = b \/ c ) let B, C be Element of Fin (DISJOINT_PAIRS A); ::_thesis: ( x in B ^ C implies ex b, c being Element of DISJOINT_PAIRS A st ( b in B & c in C & x = b \/ c ) ) assume x in B ^ C ; ::_thesis: ex b, c being Element of DISJOINT_PAIRS A st ( b in B & c in C & x = b \/ c ) then x in { (s \/ t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } by XBOOLE_0:def_4; then ex s, t being Element of DISJOINT_PAIRS A st ( x = s \/ t & s in B & t in C ) ; hence ex b, c being Element of DISJOINT_PAIRS A st ( b in B & c in C & x = b \/ c ) ; ::_thesis: verum end; theorem Th35: :: NORMFORM:35 for A being set for b, c being Element of DISJOINT_PAIRS A for B, C being Element of Fin (DISJOINT_PAIRS A) st b in B & c in C & b \/ c in DISJOINT_PAIRS A holds b \/ c in B ^ C proof let A be set ; ::_thesis: for b, c being Element of DISJOINT_PAIRS A for B, C being Element of Fin (DISJOINT_PAIRS A) st b in B & c in C & b \/ c in DISJOINT_PAIRS A holds b \/ c in B ^ C let b, c be Element of DISJOINT_PAIRS A; ::_thesis: for B, C being Element of Fin (DISJOINT_PAIRS A) st b in B & c in C & b \/ c in DISJOINT_PAIRS A holds b \/ c in B ^ C let B, C be Element of Fin (DISJOINT_PAIRS A); ::_thesis: ( b in B & c in C & b \/ c in DISJOINT_PAIRS A implies b \/ c in B ^ C ) assume ( b in B & c in C ) ; ::_thesis: ( not b \/ c in DISJOINT_PAIRS A or b \/ c in B ^ C ) then A1: b \/ c in { (s \/ t) where s, t is Element of DISJOINT_PAIRS A : ( s in B & t in C ) } ; assume b \/ c in DISJOINT_PAIRS A ; ::_thesis: b \/ c in B ^ C hence b \/ c in B ^ C by A1, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th36: :: NORMFORM:36 for A being set for a, b being Element of DISJOINT_PAIRS A for B being Element of Fin (DISJOINT_PAIRS A) st a in mi B holds ( a in B & ( b in B & b c= a implies b = a ) ) proof let A be set ; ::_thesis: for a, b being Element of DISJOINT_PAIRS A for B being Element of Fin (DISJOINT_PAIRS A) st a in mi B holds ( a in B & ( b in B & b c= a implies b = a ) ) let a, b be Element of DISJOINT_PAIRS A; ::_thesis: for B being Element of Fin (DISJOINT_PAIRS A) st a in mi B holds ( a in B & ( b in B & b c= a implies b = a ) ) let B be Element of Fin (DISJOINT_PAIRS A); ::_thesis: ( a in mi B implies ( a in B & ( b in B & b c= a implies b = a ) ) ) assume a in mi B ; ::_thesis: ( a in B & ( b in B & b c= a implies b = a ) ) then ex t being Element of DISJOINT_PAIRS A st ( a = t & ( for s being Element of DISJOINT_PAIRS A holds ( ( s in B & s c= t ) iff s = t ) ) ) ; hence ( a in B & ( b in B & b c= a implies b = a ) ) ; ::_thesis: verum end; theorem :: NORMFORM:37 for A being set for a being Element of DISJOINT_PAIRS A for B being Element of Fin (DISJOINT_PAIRS A) st a in mi B holds a in B by Th36; theorem :: NORMFORM:38 for A being set for a, b being Element of DISJOINT_PAIRS A for B being Element of Fin (DISJOINT_PAIRS A) st a in mi B & b in B & b c= a holds b = a by Th36; theorem Th39: :: NORMFORM:39 for A being set for a being Element of DISJOINT_PAIRS A for B being Element of Fin (DISJOINT_PAIRS A) st a in B & ( for b being Element of DISJOINT_PAIRS A st b in B & b c= a holds b = a ) holds a in mi B proof let A be set ; ::_thesis: for a being Element of DISJOINT_PAIRS A for B being Element of Fin (DISJOINT_PAIRS A) st a in B & ( for b being Element of DISJOINT_PAIRS A st b in B & b c= a holds b = a ) holds a in mi B let a be Element of DISJOINT_PAIRS A; ::_thesis: for B being Element of Fin (DISJOINT_PAIRS A) st a in B & ( for b being Element of DISJOINT_PAIRS A st b in B & b c= a holds b = a ) holds a in mi B let B be Element of Fin (DISJOINT_PAIRS A); ::_thesis: ( a in B & ( for b being Element of DISJOINT_PAIRS A st b in B & b c= a holds b = a ) implies a in mi B ) assume ( a in B & ( for s being Element of DISJOINT_PAIRS A st s in B & s c= a holds s = a ) ) ; ::_thesis: a in mi B then for s being Element of DISJOINT_PAIRS A holds ( ( s in B & s c= a ) iff s = a ) ; hence a in mi B ; ::_thesis: verum end; definition let A be non empty set ; let B be non empty Subset of A; let O be BinOp of B; let a, b be Element of B; :: original: . redefine funcO . (a,b) -> Element of B; coherence O . (a,b) is Element of B proof thus O . (a,b) is Element of B ; ::_thesis: verum end; end; Lm5: for A being set for B, C being Element of Fin (DISJOINT_PAIRS A) st ( for a being Element of DISJOINT_PAIRS A st a in B holds a in C ) holds B c= C proof let A be set ; ::_thesis: for B, C being Element of Fin (DISJOINT_PAIRS A) st ( for a being Element of DISJOINT_PAIRS A st a in B holds a in C ) holds B c= C let B, C be Element of Fin (DISJOINT_PAIRS A); ::_thesis: ( ( for a being Element of DISJOINT_PAIRS A st a in B holds a in C ) implies B c= C ) assume A1: for a being Element of DISJOINT_PAIRS A st a in B holds a in C ; ::_thesis: B c= C let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in C ) assume A2: x in B ; ::_thesis: x in C then x is Element of DISJOINT_PAIRS A by SETWISEO:9; hence x in C by A1, A2; ::_thesis: verum end; theorem Th40: :: NORMFORM:40 for A being set for B being Element of Fin (DISJOINT_PAIRS A) holds mi B c= B proof let A be set ; ::_thesis: for B being Element of Fin (DISJOINT_PAIRS A) holds mi B c= B let B be Element of Fin (DISJOINT_PAIRS A); ::_thesis: mi B c= B for a being Element of DISJOINT_PAIRS A st a in mi B holds a in B by Th36; hence mi B c= B by Lm5; ::_thesis: verum end; theorem Th41: :: NORMFORM:41 for A being set for b being Element of DISJOINT_PAIRS A for B being Element of Fin (DISJOINT_PAIRS A) st b in B holds ex c being Element of DISJOINT_PAIRS A st ( c c= b & c in mi B ) proof let A be set ; ::_thesis: for b being Element of DISJOINT_PAIRS A for B being Element of Fin (DISJOINT_PAIRS A) st b in B holds ex c being Element of DISJOINT_PAIRS A st ( c c= b & c in mi B ) let b be Element of DISJOINT_PAIRS A; ::_thesis: for B being Element of Fin (DISJOINT_PAIRS A) st b in B holds ex c being Element of DISJOINT_PAIRS A st ( c c= b & c in mi B ) let B be Element of Fin (DISJOINT_PAIRS A); ::_thesis: ( b in B implies ex c being Element of DISJOINT_PAIRS A st ( c c= b & c in mi B ) ) assume A1: b in B ; ::_thesis: ex c being Element of DISJOINT_PAIRS A st ( c c= b & c in mi B ) defpred S1[ Element of DISJOINT_PAIRS A, Element of DISJOINT_PAIRS A] means $1 c= $2; A2: for a being Element of DISJOINT_PAIRS A holds S1[a,a] ; A3: for a, b, c being Element of DISJOINT_PAIRS A st S1[a,b] & S1[b,c] holds S1[a,c] by Th2; for a being Element of DISJOINT_PAIRS A st a in B holds ex b being Element of DISJOINT_PAIRS A st ( b in B & S1[b,a] & ( for c being Element of DISJOINT_PAIRS A st c in B & S1[c,b] holds S1[b,c] ) ) from FRAENKEL:sch_23(A2, A3); then consider c being Element of DISJOINT_PAIRS A such that A4: c in B and A5: c c= b and A6: for a being Element of DISJOINT_PAIRS A st a in B & a c= c holds c c= a by A1; take c ; ::_thesis: ( c c= b & c in mi B ) thus c c= b by A5; ::_thesis: c in mi B now__::_thesis:_for_b_being_Element_of_DISJOINT_PAIRS_A_st_b_in_B_&_b_c=_c_holds_ b_=_c let b be Element of DISJOINT_PAIRS A; ::_thesis: ( b in B & b c= c implies b = c ) assume that A7: b in B and A8: b c= c ; ::_thesis: b = c c c= b by A6, A7, A8; hence b = c by A8, Th1; ::_thesis: verum end; hence c in mi B by A4, Th39; ::_thesis: verum end; theorem Th42: :: NORMFORM:42 for A being set for K being Element of Normal_forms_on A holds mi K = K proof let A be set ; ::_thesis: for K being Element of Normal_forms_on A holds mi K = K let K be Element of Normal_forms_on A; ::_thesis: mi K = K thus mi K c= K by Th40; :: according to XBOOLE_0:def_10 ::_thesis: K c= mi K now__::_thesis:_for_a_being_Element_of_DISJOINT_PAIRS_A_st_a_in_K_holds_ a_in_mi_K let a be Element of DISJOINT_PAIRS A; ::_thesis: ( a in K implies a in mi K ) assume A1: a in K ; ::_thesis: a in mi K then for b being Element of DISJOINT_PAIRS A st b in K & b c= a holds b = a by Th32; hence a in mi K by A1, Th39; ::_thesis: verum end; hence K c= mi K by Lm5; ::_thesis: verum end; theorem Th43: :: NORMFORM:43 for A being set for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi (B \/ C) c= (mi B) \/ C proof let A be set ; ::_thesis: for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi (B \/ C) c= (mi B) \/ C let B, C be Element of Fin (DISJOINT_PAIRS A); ::_thesis: mi (B \/ C) c= (mi B) \/ C now__::_thesis:_for_a_being_Element_of_DISJOINT_PAIRS_A_st_a_in_mi_(B_\/_C)_holds_ a_in_(mi_B)_\/_C let a be Element of DISJOINT_PAIRS A; ::_thesis: ( a in mi (B \/ C) implies a in (mi B) \/ C ) assume A1: a in mi (B \/ C) ; ::_thesis: a in (mi B) \/ C then A2: a in B \/ C by Th36; now__::_thesis:_a_in_(mi_B)_\/_C percases ( a in B or a in C ) by A2, XBOOLE_0:def_3; supposeA3: a in B ; ::_thesis: a in (mi B) \/ C now__::_thesis:_for_b_being_Element_of_DISJOINT_PAIRS_A_st_b_in_B_&_b_c=_a_holds_ b_=_a let b be Element of DISJOINT_PAIRS A; ::_thesis: ( b in B & b c= a implies b = a ) assume b in B ; ::_thesis: ( b c= a implies b = a ) then b in B \/ C by XBOOLE_0:def_3; hence ( b c= a implies b = a ) by A1, Th36; ::_thesis: verum end; then a in mi B by A3, Th39; hence a in (mi B) \/ C by XBOOLE_0:def_3; ::_thesis: verum end; suppose a in C ; ::_thesis: a in (mi B) \/ C hence a in (mi B) \/ C by XBOOLE_0:def_3; ::_thesis: verum end; end; end; hence a in (mi B) \/ C ; ::_thesis: verum end; hence mi (B \/ C) c= (mi B) \/ C by Lm5; ::_thesis: verum end; theorem Th44: :: NORMFORM:44 for A being set for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi ((mi B) \/ C) = mi (B \/ C) proof let A be set ; ::_thesis: for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi ((mi B) \/ C) = mi (B \/ C) let B, C be Element of Fin (DISJOINT_PAIRS A); ::_thesis: mi ((mi B) \/ C) = mi (B \/ C) A1: (mi B) \/ C c= B \/ C by Th40, XBOOLE_1:9; now__::_thesis:_for_a_being_Element_of_DISJOINT_PAIRS_A_st_a_in_mi_((mi_B)_\/_C)_holds_ a_in_mi_(B_\/_C) let a be Element of DISJOINT_PAIRS A; ::_thesis: ( a in mi ((mi B) \/ C) implies a in mi (B \/ C) ) assume A2: a in mi ((mi B) \/ C) ; ::_thesis: a in mi (B \/ C) A3: now__::_thesis:_for_b_being_Element_of_DISJOINT_PAIRS_A_st_b_in_B_\/_C_&_b_c=_a_holds_ b_=_a let b be Element of DISJOINT_PAIRS A; ::_thesis: ( b in B \/ C & b c= a implies b = a ) assume that A4: b in B \/ C and A5: b c= a ; ::_thesis: b = a now__::_thesis:_b_=_a percases ( b in B or b in C ) by A4, XBOOLE_0:def_3; suppose b in B ; ::_thesis: b = a then consider c being Element of DISJOINT_PAIRS A such that A6: c c= b and A7: c in mi B by Th41; ( c in (mi B) \/ C & c c= a ) by A5, A6, A7, Th2, XBOOLE_0:def_3; then c = a by A2, Th36; hence b = a by A5, A6, Th1; ::_thesis: verum end; suppose b in C ; ::_thesis: b = a then b in (mi B) \/ C by XBOOLE_0:def_3; hence b = a by A2, A5, Th36; ::_thesis: verum end; end; end; hence b = a ; ::_thesis: verum end; a in (mi B) \/ C by A2, Th36; hence a in mi (B \/ C) by A1, A3, Th39; ::_thesis: verum end; hence mi ((mi B) \/ C) c= mi (B \/ C) by Lm5; :: according to XBOOLE_0:def_10 ::_thesis: mi (B \/ C) c= mi ((mi B) \/ C) A8: mi (B \/ C) c= (mi B) \/ C by Th43; now__::_thesis:_for_a_being_Element_of_DISJOINT_PAIRS_A_st_a_in_mi_(B_\/_C)_holds_ a_in_mi_((mi_B)_\/_C) let a be Element of DISJOINT_PAIRS A; ::_thesis: ( a in mi (B \/ C) implies a in mi ((mi B) \/ C) ) assume A9: a in mi (B \/ C) ; ::_thesis: a in mi ((mi B) \/ C) then for b being Element of DISJOINT_PAIRS A st b in (mi B) \/ C & b c= a holds b = a by A1, Th36; hence a in mi ((mi B) \/ C) by A8, A9, Th39; ::_thesis: verum end; hence mi (B \/ C) c= mi ((mi B) \/ C) by Lm5; ::_thesis: verum end; theorem :: NORMFORM:45 for A being set for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi (B \/ (mi C)) = mi (B \/ C) by Th44; theorem Th46: :: NORMFORM:46 for A being set for B, C, D being Element of Fin (DISJOINT_PAIRS A) st B c= C holds B ^ D c= C ^ D proof let A be set ; ::_thesis: for B, C, D being Element of Fin (DISJOINT_PAIRS A) st B c= C holds B ^ D c= C ^ D let B, C, D be Element of Fin (DISJOINT_PAIRS A); ::_thesis: ( B c= C implies B ^ D c= C ^ D ) deffunc H1( Element of DISJOINT_PAIRS A, Element of DISJOINT_PAIRS A) -> Element of [:(Fin A),(Fin A):] = $1 \/ $2; defpred S1[ set , set ] means ( $1 in B & $2 in D ); defpred S2[ set , set ] means ( $1 in C & $2 in D ); set X1 = { H1(s,t) where s, t is Element of DISJOINT_PAIRS A : S1[s,t] } ; set X2 = { H1(s,t) where s, t is Element of DISJOINT_PAIRS A : S2[s,t] } ; assume B c= C ; ::_thesis: B ^ D c= C ^ D then A1: for s, t being Element of DISJOINT_PAIRS A st S1[s,t] holds S2[s,t] ; { H1(s,t) where s, t is Element of DISJOINT_PAIRS A : S1[s,t] } c= { H1(s,t) where s, t is Element of DISJOINT_PAIRS A : S2[s,t] } from FRAENKEL:sch_2(A1); hence B ^ D c= C ^ D by XBOOLE_1:26; ::_thesis: verum end; Lm6: for A being set for a being Element of DISJOINT_PAIRS A for B, C being Element of Fin (DISJOINT_PAIRS A) st a in B ^ C holds ex b being Element of DISJOINT_PAIRS A st ( b c= a & b in (mi B) ^ C ) proof let A be set ; ::_thesis: for a being Element of DISJOINT_PAIRS A for B, C being Element of Fin (DISJOINT_PAIRS A) st a in B ^ C holds ex b being Element of DISJOINT_PAIRS A st ( b c= a & b in (mi B) ^ C ) let a be Element of DISJOINT_PAIRS A; ::_thesis: for B, C being Element of Fin (DISJOINT_PAIRS A) st a in B ^ C holds ex b being Element of DISJOINT_PAIRS A st ( b c= a & b in (mi B) ^ C ) let B, C be Element of Fin (DISJOINT_PAIRS A); ::_thesis: ( a in B ^ C implies ex b being Element of DISJOINT_PAIRS A st ( b c= a & b in (mi B) ^ C ) ) assume a in B ^ C ; ::_thesis: ex b being Element of DISJOINT_PAIRS A st ( b c= a & b in (mi B) ^ C ) then consider b, c being Element of DISJOINT_PAIRS A such that A1: b in B and A2: c in C and A3: a = b \/ c by Th34; consider d being Element of DISJOINT_PAIRS A such that A4: d c= b and A5: d in mi B by A1, Th41; d \/ c c= a by A3, A4, Th12; then reconsider e = d \/ c as Element of DISJOINT_PAIRS A by Th26; take e ; ::_thesis: ( e c= a & e in (mi B) ^ C ) thus e c= a by A3, A4, Th12; ::_thesis: e in (mi B) ^ C thus e in (mi B) ^ C by A2, A5, Th35; ::_thesis: verum end; theorem Th47: :: NORMFORM:47 for A being set for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi (B ^ C) c= (mi B) ^ C proof let A be set ; ::_thesis: for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi (B ^ C) c= (mi B) ^ C let B, C be Element of Fin (DISJOINT_PAIRS A); ::_thesis: mi (B ^ C) c= (mi B) ^ C A1: (mi B) ^ C c= B ^ C by Th40, Th46; now__::_thesis:_for_a_being_Element_of_DISJOINT_PAIRS_A_st_a_in_mi_(B_^_C)_holds_ a_in_(mi_B)_^_C let a be Element of DISJOINT_PAIRS A; ::_thesis: ( a in mi (B ^ C) implies a in (mi B) ^ C ) assume A2: a in mi (B ^ C) ; ::_thesis: a in (mi B) ^ C then a in B ^ C by Th36; then ex b being Element of DISJOINT_PAIRS A st ( b c= a & b in (mi B) ^ C ) by Lm6; hence a in (mi B) ^ C by A1, A2, Th36; ::_thesis: verum end; hence mi (B ^ C) c= (mi B) ^ C by Lm5; ::_thesis: verum end; theorem Th48: :: NORMFORM:48 for A being set for B, C being Element of Fin (DISJOINT_PAIRS A) holds B ^ C = C ^ B proof let A be set ; ::_thesis: for B, C being Element of Fin (DISJOINT_PAIRS A) holds B ^ C = C ^ B let B, C be Element of Fin (DISJOINT_PAIRS A); ::_thesis: B ^ C = C ^ B deffunc H1( Element of DISJOINT_PAIRS A, Element of DISJOINT_PAIRS A) -> Element of [:(Fin A),(Fin A):] = $1 \/ $2; defpred S1[ set , set ] means ( $1 in B & $2 in C ); defpred S2[ set , set ] means ( $2 in C & $1 in B ); set X1 = { H1(s,t) where s, t is Element of DISJOINT_PAIRS A : S1[s,t] } ; set X2 = { H1(t,s) where s, t is Element of DISJOINT_PAIRS A : S2[s,t] } ; A1: for s, t being Element of DISJOINT_PAIRS A holds H1(s,t) = H1(t,s) ; A2: now__::_thesis:_for_x_being_set_holds_ (_x_in__{__H1(t,s)_where_s,_t_is_Element_of_DISJOINT_PAIRS_A_:_S2[s,t]__}__iff_x_in__{__(t_\/_s)_where_t,_s_is_Element_of_DISJOINT_PAIRS_A_:_(_t_in_C_&_s_in_B_)__}__) let x be set ; ::_thesis: ( x in { H1(t,s) where s, t is Element of DISJOINT_PAIRS A : S2[s,t] } iff x in { (t \/ s) where t, s is Element of DISJOINT_PAIRS A : ( t in C & s in B ) } ) ( x in { H1(t,s) where s, t is Element of DISJOINT_PAIRS A : S2[s,t] } iff ex s, t being Element of DISJOINT_PAIRS A st ( x = t \/ s & t in C & s in B ) ) ; then ( x in { H1(t,s) where s, t is Element of DISJOINT_PAIRS A : S2[s,t] } iff ex t, s being Element of DISJOINT_PAIRS A st ( x = t \/ s & t in C & s in B ) ) ; hence ( x in { H1(t,s) where s, t is Element of DISJOINT_PAIRS A : S2[s,t] } iff x in { (t \/ s) where t, s is Element of DISJOINT_PAIRS A : ( t in C & s in B ) } ) ; ::_thesis: verum end; A3: for s, t being Element of DISJOINT_PAIRS A holds ( S1[s,t] iff S2[s,t] ) ; { H1(s,t) where s, t is Element of DISJOINT_PAIRS A : S1[s,t] } = { H1(t,s) where s, t is Element of DISJOINT_PAIRS A : S2[s,t] } from FRAENKEL:sch_8(A3, A1); hence B ^ C = C ^ B by A2, TARSKI:1; ::_thesis: verum end; theorem Th49: :: NORMFORM:49 for A being set for B, C, D being Element of Fin (DISJOINT_PAIRS A) st B c= C holds D ^ B c= D ^ C proof let A be set ; ::_thesis: for B, C, D being Element of Fin (DISJOINT_PAIRS A) st B c= C holds D ^ B c= D ^ C let B, C, D be Element of Fin (DISJOINT_PAIRS A); ::_thesis: ( B c= C implies D ^ B c= D ^ C ) ( D ^ C = C ^ D & D ^ B = B ^ D ) by Th48; hence ( B c= C implies D ^ B c= D ^ C ) by Th46; ::_thesis: verum end; theorem Th50: :: NORMFORM:50 for A being set for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi ((mi B) ^ C) = mi (B ^ C) proof let A be set ; ::_thesis: for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi ((mi B) ^ C) = mi (B ^ C) let B, C be Element of Fin (DISJOINT_PAIRS A); ::_thesis: mi ((mi B) ^ C) = mi (B ^ C) A1: (mi B) ^ C c= B ^ C by Th40, Th46; now__::_thesis:_for_a_being_Element_of_DISJOINT_PAIRS_A_st_a_in_mi_((mi_B)_^_C)_holds_ a_in_mi_(B_^_C) let a be Element of DISJOINT_PAIRS A; ::_thesis: ( a in mi ((mi B) ^ C) implies a in mi (B ^ C) ) assume A2: a in mi ((mi B) ^ C) ; ::_thesis: a in mi (B ^ C) A3: now__::_thesis:_for_b_being_Element_of_DISJOINT_PAIRS_A_st_b_in_B_^_C_&_b_c=_a_holds_ b_=_a let b be Element of DISJOINT_PAIRS A; ::_thesis: ( b in B ^ C & b c= a implies b = a ) assume b in B ^ C ; ::_thesis: ( b c= a implies b = a ) then consider c being Element of DISJOINT_PAIRS A such that A4: c c= b and A5: c in (mi B) ^ C by Lm6; assume A6: b c= a ; ::_thesis: b = a then c c= a by A4, Th2; then c = a by A2, A5, Th36; hence b = a by A4, A6, Th1; ::_thesis: verum end; a in (mi B) ^ C by A2, Th36; hence a in mi (B ^ C) by A1, A3, Th39; ::_thesis: verum end; hence mi ((mi B) ^ C) c= mi (B ^ C) by Lm5; :: according to XBOOLE_0:def_10 ::_thesis: mi (B ^ C) c= mi ((mi B) ^ C) A7: mi (B ^ C) c= (mi B) ^ C by Th47; now__::_thesis:_for_a_being_Element_of_DISJOINT_PAIRS_A_st_a_in_mi_(B_^_C)_holds_ a_in_mi_((mi_B)_^_C) let a be Element of DISJOINT_PAIRS A; ::_thesis: ( a in mi (B ^ C) implies a in mi ((mi B) ^ C) ) assume A8: a in mi (B ^ C) ; ::_thesis: a in mi ((mi B) ^ C) then for b being Element of DISJOINT_PAIRS A st b in (mi B) ^ C & b c= a holds b = a by A1, Th36; hence a in mi ((mi B) ^ C) by A7, A8, Th39; ::_thesis: verum end; hence mi (B ^ C) c= mi ((mi B) ^ C) by Lm5; ::_thesis: verum end; theorem Th51: :: NORMFORM:51 for A being set for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi (B ^ (mi C)) = mi (B ^ C) proof let A be set ; ::_thesis: for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi (B ^ (mi C)) = mi (B ^ C) let B, C be Element of Fin (DISJOINT_PAIRS A); ::_thesis: mi (B ^ (mi C)) = mi (B ^ C) ( B ^ (mi C) = (mi C) ^ B & B ^ C = C ^ B ) by Th48; hence mi (B ^ (mi C)) = mi (B ^ C) by Th50; ::_thesis: verum end; theorem Th52: :: NORMFORM:52 for A being set for K, L, M being Element of Normal_forms_on A holds K ^ (L ^ M) = (K ^ L) ^ M proof let A be set ; ::_thesis: for K, L, M being Element of Normal_forms_on A holds K ^ (L ^ M) = (K ^ L) ^ M let K, L, M be Element of Normal_forms_on A; ::_thesis: K ^ (L ^ M) = (K ^ L) ^ M A1: ( L ^ M = M ^ L & K ^ L = L ^ K ) by Th48; A2: now__::_thesis:_for_K,_L,_M_being_Element_of_Normal_forms_on_A_holds_K_^_(L_^_M)_c=_(K_^_L)_^_M let K, L, M be Element of Normal_forms_on A; ::_thesis: K ^ (L ^ M) c= (K ^ L) ^ M now__::_thesis:_for_a_being_Element_of_DISJOINT_PAIRS_A_st_a_in_K_^_(L_^_M)_holds_ a_in_(K_^_L)_^_M let a be Element of DISJOINT_PAIRS A; ::_thesis: ( a in K ^ (L ^ M) implies a in (K ^ L) ^ M ) assume a in K ^ (L ^ M) ; ::_thesis: a in (K ^ L) ^ M then consider b, c being Element of DISJOINT_PAIRS A such that A3: b in K and A4: c in L ^ M and A5: a = b \/ c by Th34; consider b1, c1 being Element of DISJOINT_PAIRS A such that A6: b1 in L and A7: c1 in M and A8: c = b1 \/ c1 by A4, Th34; reconsider d = b \/ (b1 \/ c1) as Element of DISJOINT_PAIRS A by A5, A8; A9: b \/ (b1 \/ c1) = (b \/ b1) \/ c1 by Th3; then b \/ b1 c= d by Th10; then reconsider c2 = b \/ b1 as Element of DISJOINT_PAIRS A by Th26; c2 in K ^ L by A3, A6, Th35; hence a in (K ^ L) ^ M by A5, A7, A8, A9, Th35; ::_thesis: verum end; hence K ^ (L ^ M) c= (K ^ L) ^ M by Lm5; ::_thesis: verum end; then A10: K ^ (L ^ M) c= (K ^ L) ^ M ; ( (K ^ L) ^ M = M ^ (K ^ L) & K ^ (L ^ M) = (L ^ M) ^ K ) by Th48; then (K ^ L) ^ M c= K ^ (L ^ M) by A1, A2; hence K ^ (L ^ M) = (K ^ L) ^ M by A10, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th53: :: NORMFORM:53 for A being set for K, L, M being Element of Normal_forms_on A holds K ^ (L \/ M) = (K ^ L) \/ (K ^ M) proof let A be set ; ::_thesis: for K, L, M being Element of Normal_forms_on A holds K ^ (L \/ M) = (K ^ L) \/ (K ^ M) let K, L, M be Element of Normal_forms_on A; ::_thesis: K ^ (L \/ M) = (K ^ L) \/ (K ^ M) now__::_thesis:_for_a_being_Element_of_DISJOINT_PAIRS_A_st_a_in_K_^_(L_\/_M)_holds_ a_in_(K_^_L)_\/_(K_^_M) let a be Element of DISJOINT_PAIRS A; ::_thesis: ( a in K ^ (L \/ M) implies a in (K ^ L) \/ (K ^ M) ) assume a in K ^ (L \/ M) ; ::_thesis: a in (K ^ L) \/ (K ^ M) then consider b, c being Element of DISJOINT_PAIRS A such that A1: b in K and A2: c in L \/ M and A3: a = b \/ c by Th34; ( c in L or c in M ) by A2, XBOOLE_0:def_3; then ( a in K ^ L or a in K ^ M ) by A1, A3, Th35; hence a in (K ^ L) \/ (K ^ M) by XBOOLE_0:def_3; ::_thesis: verum end; hence K ^ (L \/ M) c= (K ^ L) \/ (K ^ M) by Lm5; :: according to XBOOLE_0:def_10 ::_thesis: (K ^ L) \/ (K ^ M) c= K ^ (L \/ M) ( K ^ L c= K ^ (L \/ M) & K ^ M c= K ^ (L \/ M) ) by Th49, XBOOLE_1:7; hence (K ^ L) \/ (K ^ M) c= K ^ (L \/ M) by XBOOLE_1:8; ::_thesis: verum end; Lm7: for A being set for a being Element of DISJOINT_PAIRS A for B, C being Element of Fin (DISJOINT_PAIRS A) st a in B ^ C holds ex c being Element of DISJOINT_PAIRS A st ( c in C & c c= a ) proof let A be set ; ::_thesis: for a being Element of DISJOINT_PAIRS A for B, C being Element of Fin (DISJOINT_PAIRS A) st a in B ^ C holds ex c being Element of DISJOINT_PAIRS A st ( c in C & c c= a ) let a be Element of DISJOINT_PAIRS A; ::_thesis: for B, C being Element of Fin (DISJOINT_PAIRS A) st a in B ^ C holds ex c being Element of DISJOINT_PAIRS A st ( c in C & c c= a ) let B, C be Element of Fin (DISJOINT_PAIRS A); ::_thesis: ( a in B ^ C implies ex c being Element of DISJOINT_PAIRS A st ( c in C & c c= a ) ) assume a in B ^ C ; ::_thesis: ex c being Element of DISJOINT_PAIRS A st ( c in C & c c= a ) then consider b, c being Element of DISJOINT_PAIRS A such that b in B and A1: c in C and A2: a = b \/ c by Th34; take c ; ::_thesis: ( c in C & c c= a ) thus c in C by A1; ::_thesis: c c= a thus c c= a by A2, Th10; ::_thesis: verum end; Lm8: for A being set for K, L being Element of Normal_forms_on A holds mi ((K ^ L) \/ L) = mi L proof let A be set ; ::_thesis: for K, L being Element of Normal_forms_on A holds mi ((K ^ L) \/ L) = mi L let K, L be Element of Normal_forms_on A; ::_thesis: mi ((K ^ L) \/ L) = mi L now__::_thesis:_for_a_being_Element_of_DISJOINT_PAIRS_A_st_a_in_mi_((K_^_L)_\/_L)_holds_ a_in_mi_L let a be Element of DISJOINT_PAIRS A; ::_thesis: ( a in mi ((K ^ L) \/ L) implies a in mi L ) assume A1: a in mi ((K ^ L) \/ L) ; ::_thesis: a in mi L A2: now__::_thesis:_for_b_being_Element_of_DISJOINT_PAIRS_A_st_b_in_L_&_b_c=_a_holds_ b_=_a let b be Element of DISJOINT_PAIRS A; ::_thesis: ( b in L & b c= a implies b = a ) assume b in L ; ::_thesis: ( b c= a implies b = a ) then b in (K ^ L) \/ L by XBOOLE_0:def_3; hence ( b c= a implies b = a ) by A1, Th36; ::_thesis: verum end; A3: now__::_thesis:_(_a_in_K_^_L_implies_a_in_L_) assume a in K ^ L ; ::_thesis: a in L then consider b being Element of DISJOINT_PAIRS A such that A4: b in L and A5: b c= a by Lm7; b in (K ^ L) \/ L by A4, XBOOLE_0:def_3; hence a in L by A1, A4, A5, Th36; ::_thesis: verum end; a in (K ^ L) \/ L by A1, Th36; then ( a in K ^ L or a in L ) by XBOOLE_0:def_3; hence a in mi L by A3, A2, Th39; ::_thesis: verum end; hence mi ((K ^ L) \/ L) c= mi L by Lm5; :: according to XBOOLE_0:def_10 ::_thesis: mi L c= mi ((K ^ L) \/ L) now__::_thesis:_for_a_being_Element_of_DISJOINT_PAIRS_A_st_a_in_mi_L_holds_ a_in_mi_((K_^_L)_\/_L) let a be Element of DISJOINT_PAIRS A; ::_thesis: ( a in mi L implies a in mi ((K ^ L) \/ L) ) assume A6: a in mi L ; ::_thesis: a in mi ((K ^ L) \/ L) then A7: a in L by Th36; A8: now__::_thesis:_for_b_being_Element_of_DISJOINT_PAIRS_A_st_b_in_(K_^_L)_\/_L_&_b_c=_a_holds_ b_=_a let b be Element of DISJOINT_PAIRS A; ::_thesis: ( b in (K ^ L) \/ L & b c= a implies b = a ) assume b in (K ^ L) \/ L ; ::_thesis: ( b c= a implies b = a ) then A9: ( b in K ^ L or b in L ) by XBOOLE_0:def_3; assume A10: b c= a ; ::_thesis: b = a now__::_thesis:_(_b_in_K_^_L_implies_b_in_L_) assume b in K ^ L ; ::_thesis: b in L then consider c being Element of DISJOINT_PAIRS A such that A11: c in L and A12: c c= b by Lm7; c c= a by A10, A12, Th2; then c = a by A6, A11, Th36; hence b in L by A7, A10, A12, Th1; ::_thesis: verum end; hence b = a by A6, A9, A10, Th36; ::_thesis: verum end; a in (K ^ L) \/ L by A7, XBOOLE_0:def_3; hence a in mi ((K ^ L) \/ L) by A8, Th39; ::_thesis: verum end; hence mi L c= mi ((K ^ L) \/ L) by Lm5; ::_thesis: verum end; theorem Th54: :: NORMFORM:54 for A being set for B being Element of Fin (DISJOINT_PAIRS A) holds B c= B ^ B proof let A be set ; ::_thesis: for B being Element of Fin (DISJOINT_PAIRS A) holds B c= B ^ B let B be Element of Fin (DISJOINT_PAIRS A); ::_thesis: B c= B ^ B now__::_thesis:_for_a_being_Element_of_DISJOINT_PAIRS_A_st_a_in_B_holds_ a_in_B_^_B let a be Element of DISJOINT_PAIRS A; ::_thesis: ( a in B implies a in B ^ B ) a = a \/ a ; hence ( a in B implies a in B ^ B ) by Th35; ::_thesis: verum end; hence B c= B ^ B by Lm5; ::_thesis: verum end; theorem Th55: :: NORMFORM:55 for A being set for K being Element of Normal_forms_on A holds mi (K ^ K) = mi K proof let A be set ; ::_thesis: for K being Element of Normal_forms_on A holds mi (K ^ K) = mi K let K be Element of Normal_forms_on A; ::_thesis: mi (K ^ K) = mi K thus mi (K ^ K) = mi ((K ^ K) \/ K) by Th54, XBOOLE_1:12 .= mi K by Lm8 ; ::_thesis: verum end; definition let A be set ; func NormForm A -> strict LattStr means :Def12: :: NORMFORM:def 12 ( the carrier of it = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds ( the L_join of it . (B,C) = mi (B \/ C) & the L_meet of it . (B,C) = mi (B ^ C) ) ) ); existence ex b1 being strict LattStr st ( the carrier of b1 = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds ( the L_join of b1 . (B,C) = mi (B \/ C) & the L_meet of b1 . (B,C) = mi (B ^ C) ) ) ) proof set L = Normal_forms_on A; deffunc H1( Element of Normal_forms_on A, Element of Normal_forms_on A) -> Element of Normal_forms_on A = mi ($1 \/ $2); consider j being BinOp of (Normal_forms_on A) such that A1: for x, y being Element of Normal_forms_on A holds j . (x,y) = H1(x,y) from BINOP_1:sch_4(); deffunc H2( Element of Normal_forms_on A, Element of Normal_forms_on A) -> Element of Normal_forms_on A = mi ($1 ^ $2); consider m being BinOp of (Normal_forms_on A) such that A2: for x, y being Element of Normal_forms_on A holds m . (x,y) = H2(x,y) from BINOP_1:sch_4(); take LattStr(# (Normal_forms_on A),j,m #) ; ::_thesis: ( the carrier of LattStr(# (Normal_forms_on A),j,m #) = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds ( the L_join of LattStr(# (Normal_forms_on A),j,m #) . (B,C) = mi (B \/ C) & the L_meet of LattStr(# (Normal_forms_on A),j,m #) . (B,C) = mi (B ^ C) ) ) ) thus ( the carrier of LattStr(# (Normal_forms_on A),j,m #) = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds ( the L_join of LattStr(# (Normal_forms_on A),j,m #) . (B,C) = mi (B \/ C) & the L_meet of LattStr(# (Normal_forms_on A),j,m #) . (B,C) = mi (B ^ C) ) ) ) by A1, A2; ::_thesis: verum end; uniqueness for b1, b2 being strict LattStr st the carrier of b1 = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds ( the L_join of b1 . (B,C) = mi (B \/ C) & the L_meet of b1 . (B,C) = mi (B ^ C) ) ) & the carrier of b2 = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds ( the L_join of b2 . (B,C) = mi (B \/ C) & the L_meet of b2 . (B,C) = mi (B ^ C) ) ) holds b1 = b2 proof set L = Normal_forms_on A; let A1, A2 be strict LattStr ; ::_thesis: ( the carrier of A1 = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds ( the L_join of A1 . (B,C) = mi (B \/ C) & the L_meet of A1 . (B,C) = mi (B ^ C) ) ) & the carrier of A2 = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds ( the L_join of A2 . (B,C) = mi (B \/ C) & the L_meet of A2 . (B,C) = mi (B ^ C) ) ) implies A1 = A2 ) assume that A3: the carrier of A1 = Normal_forms_on A and A4: for A, B being Element of Normal_forms_on A holds ( the L_join of A1 . (A,B) = mi (A \/ B) & the L_meet of A1 . (A,B) = mi (A ^ B) ) and A5: the carrier of A2 = Normal_forms_on A and A6: for A, B being Element of Normal_forms_on A holds ( the L_join of A2 . (A,B) = mi (A \/ B) & the L_meet of A2 . (A,B) = mi (A ^ B) ) ; ::_thesis: A1 = A2 reconsider a3 = the L_meet of A1, a4 = the L_meet of A2, a1 = the L_join of A1, a2 = the L_join of A2 as BinOp of (Normal_forms_on A) by A3, A5; now__::_thesis:_for_x,_y_being_Element_of_Normal_forms_on_A_holds_a1_._(x,y)_=_a2_._(x,y) let x, y be Element of Normal_forms_on A; ::_thesis: a1 . (x,y) = a2 . (x,y) thus a1 . (x,y) = mi (x \/ y) by A4 .= a2 . (x,y) by A6 ; ::_thesis: verum end; then A7: a1 = a2 by BINOP_1:2; now__::_thesis:_for_x,_y_being_Element_of_Normal_forms_on_A_holds_a3_._(x,y)_=_a4_._(x,y) let x, y be Element of Normal_forms_on A; ::_thesis: a3 . (x,y) = a4 . (x,y) thus a3 . (x,y) = mi (x ^ y) by A4 .= a4 . (x,y) by A6 ; ::_thesis: verum end; hence A1 = A2 by A3, A5, A7, BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def12 defines NormForm NORMFORM:def_12_:_ for A being set for b2 being strict LattStr holds ( b2 = NormForm A iff ( the carrier of b2 = Normal_forms_on A & ( for B, C being Element of Normal_forms_on A holds ( the L_join of b2 . (B,C) = mi (B \/ C) & the L_meet of b2 . (B,C) = mi (B ^ C) ) ) ) ); registration let A be set ; cluster NormForm A -> non empty strict ; coherence not NormForm A is empty proof the carrier of (NormForm A) = Normal_forms_on A by Def12; hence not NormForm A is empty ; ::_thesis: verum end; end; Lm9: for A being set for a, b being Element of (NormForm A) holds a "\/" b = b "\/" a proof let A be set ; ::_thesis: for a, b being Element of (NormForm A) holds a "\/" b = b "\/" a set G = NormForm A; let a, b be Element of (NormForm A); ::_thesis: a "\/" b = b "\/" a reconsider a9 = a, b9 = b as Element of Normal_forms_on A by Def12; a "\/" b = mi (b9 \/ a9) by Def12 .= b "\/" a by Def12 ; hence a "\/" b = b "\/" a ; ::_thesis: verum end; Lm10: for A being set for a, b, c being Element of (NormForm A) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c proof let A be set ; ::_thesis: for a, b, c being Element of (NormForm A) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c set G = NormForm A; let a, b, c be Element of (NormForm A); ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c reconsider a9 = a, b9 = b, c9 = c as Element of Normal_forms_on A by Def12; a "\/" (b "\/" c) = the L_join of (NormForm A) . (a,(mi (b9 \/ c9))) by Def12 .= mi ((mi (b9 \/ c9)) \/ a9) by Def12 .= mi (a9 \/ (b9 \/ c9)) by Th44 .= mi ((a9 \/ b9) \/ c9) by XBOOLE_1:4 .= mi ((mi (a9 \/ b9)) \/ c9) by Th44 .= the L_join of (NormForm A) . ((mi (a9 \/ b9)),c9) by Def12 .= (a "\/" b) "\/" c by Def12 ; hence a "\/" (b "\/" c) = (a "\/" b) "\/" c ; ::_thesis: verum end; Lm11: for A being set for K, L being Element of Normal_forms_on A holds the L_join of (NormForm A) . (( the L_meet of (NormForm A) . (K,L)),L) = L proof let A be set ; ::_thesis: for K, L being Element of Normal_forms_on A holds the L_join of (NormForm A) . (( the L_meet of (NormForm A) . (K,L)),L) = L let K, L be Element of Normal_forms_on A; ::_thesis: the L_join of (NormForm A) . (( the L_meet of (NormForm A) . (K,L)),L) = L thus the L_join of (NormForm A) . (( the L_meet of (NormForm A) . (K,L)),L) = the L_join of (NormForm A) . ((mi (K ^ L)),L) by Def12 .= mi ((mi (K ^ L)) \/ L) by Def12 .= mi ((K ^ L) \/ L) by Th44 .= mi L by Lm8 .= L by Th42 ; ::_thesis: verum end; Lm12: for A being set for a, b being Element of (NormForm A) holds (a "/\" b) "\/" b = b proof let A be set ; ::_thesis: for a, b being Element of (NormForm A) holds (a "/\" b) "\/" b = b let a, b be Element of (NormForm A); ::_thesis: (a "/\" b) "\/" b = b reconsider a9 = a, b9 = b as Element of Normal_forms_on A by Def12; set G = NormForm A; thus (a "/\" b) "\/" b = the L_join of (NormForm A) . (( the L_meet of (NormForm A) . (a9,b9)),b9) .= b by Lm11 ; ::_thesis: verum end; Lm13: for A being set for a, b being Element of (NormForm A) holds a "/\" b = b "/\" a proof let A be set ; ::_thesis: for a, b being Element of (NormForm A) holds a "/\" b = b "/\" a set G = NormForm A; let a, b be Element of (NormForm A); ::_thesis: a "/\" b = b "/\" a reconsider a9 = a, b9 = b as Element of Normal_forms_on A by Def12; a "/\" b = mi (a9 ^ b9) by Def12 .= mi (b9 ^ a9) by Th48 .= b "/\" a by Def12 ; hence a "/\" b = b "/\" a ; ::_thesis: verum end; Lm14: for A being set for a, b, c being Element of (NormForm A) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c proof let A be set ; ::_thesis: for a, b, c being Element of (NormForm A) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c set G = NormForm A; let a, b, c be Element of (NormForm A); ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c reconsider a9 = a, b9 = b, c9 = c as Element of Normal_forms_on A by Def12; a "/\" (b "/\" c) = the L_meet of (NormForm A) . (a,(mi (b9 ^ c9))) by Def12 .= mi (a9 ^ (mi (b9 ^ c9))) by Def12 .= mi (a9 ^ (b9 ^ c9)) by Th51 .= mi ((a9 ^ b9) ^ c9) by Th52 .= mi ((mi (a9 ^ b9)) ^ c9) by Th50 .= the L_meet of (NormForm A) . ((mi (a9 ^ b9)),c9) by Def12 .= (a "/\" b) "/\" c by Def12 ; hence a "/\" (b "/\" c) = (a "/\" b) "/\" c ; ::_thesis: verum end; Lm15: for A being set for K, L, M being Element of Normal_forms_on A holds the L_meet of (NormForm A) . (K,( the L_join of (NormForm A) . (L,M))) = the L_join of (NormForm A) . (( the L_meet of (NormForm A) . (K,L)),( the L_meet of (NormForm A) . (K,M))) proof let A be set ; ::_thesis: for K, L, M being Element of Normal_forms_on A holds the L_meet of (NormForm A) . (K,( the L_join of (NormForm A) . (L,M))) = the L_join of (NormForm A) . (( the L_meet of (NormForm A) . (K,L)),( the L_meet of (NormForm A) . (K,M))) let K, L, M be Element of Normal_forms_on A; ::_thesis: the L_meet of (NormForm A) . (K,( the L_join of (NormForm A) . (L,M))) = the L_join of (NormForm A) . (( the L_meet of (NormForm A) . (K,L)),( the L_meet of (NormForm A) . (K,M))) A1: the L_meet of (NormForm A) . (K,M) = mi (K ^ M) by Def12; ( the L_join of (NormForm A) . (L,M) = mi (L \/ M) & the L_meet of (NormForm A) . (K,L) = mi (K ^ L) ) by Def12; then reconsider La = the L_join of (NormForm A) . (L,M), Lb = the L_meet of (NormForm A) . (K,L), Lc = the L_meet of (NormForm A) . (K,M) as Element of Normal_forms_on A by A1; the L_meet of (NormForm A) . (K,( the L_join of (NormForm A) . (L,M))) = mi (K ^ La) by Def12 .= mi (K ^ (mi (L \/ M))) by Def12 .= mi (K ^ (L \/ M)) by Th51 .= mi ((K ^ L) \/ (K ^ M)) by Th53 .= mi ((mi (K ^ L)) \/ (K ^ M)) by Th44 .= mi ((mi (K ^ L)) \/ (mi (K ^ M))) by Th44 .= mi (Lb \/ (mi (K ^ M))) by Def12 .= mi (Lb \/ Lc) by Def12 ; hence the L_meet of (NormForm A) . (K,( the L_join of (NormForm A) . (L,M))) = the L_join of (NormForm A) . (( the L_meet of (NormForm A) . (K,L)),( the L_meet of (NormForm A) . (K,M))) by Def12; ::_thesis: verum end; Lm16: for A being set for a, b being Element of (NormForm A) holds a "/\" (a "\/" b) = a proof let A be set ; ::_thesis: for a, b being Element of (NormForm A) holds a "/\" (a "\/" b) = a set G = NormForm A; let a, b be Element of (NormForm A); ::_thesis: a "/\" (a "\/" b) = a reconsider a9 = a, b9 = b as Element of Normal_forms_on A by Def12; thus a "/\" (a "\/" b) = the L_join of (NormForm A) . (( the L_meet of (NormForm A) . (a9,a9)),( the L_meet of (NormForm A) . (a9,b9))) by Lm15 .= the L_join of (NormForm A) . ((mi (a9 ^ a9)),( the L_meet of (NormForm A) . (a9,b9))) by Def12 .= the L_join of (NormForm A) . ((mi a9),( the L_meet of (NormForm A) . (a9,b9))) by Th55 .= a "\/" (a "/\" b) by Th42 .= (a "/\" b) "\/" a by Lm9 .= (b "/\" a) "\/" a by Lm13 .= a by Lm12 ; ::_thesis: verum end; registration let A be set ; cluster NormForm A -> strict Lattice-like ; coherence NormForm A is Lattice-like proof set G = NormForm A; thus for u, v being Element of (NormForm A) holds u "\/" v = v "\/" u by Lm9; :: according to LATTICES:def_4,LATTICES:def_10 ::_thesis: ( NormForm A is join-associative & NormForm A is meet-absorbing & NormForm A is meet-commutative & NormForm A is meet-associative & NormForm A is join-absorbing ) thus for u, v, w being Element of (NormForm A) holds u "\/" (v "\/" w) = (u "\/" v) "\/" w by Lm10; :: according to LATTICES:def_5 ::_thesis: ( NormForm A is meet-absorbing & NormForm A is meet-commutative & NormForm A is meet-associative & NormForm A is join-absorbing ) thus for u, v being Element of (NormForm A) holds (u "/\" v) "\/" v = v by Lm12; :: according to LATTICES:def_8 ::_thesis: ( NormForm A is meet-commutative & NormForm A is meet-associative & NormForm A is join-absorbing ) thus for u, v being Element of (NormForm A) holds u "/\" v = v "/\" u by Lm13; :: according to LATTICES:def_6 ::_thesis: ( NormForm A is meet-associative & NormForm A is join-absorbing ) thus for u, v, w being Element of (NormForm A) holds u "/\" (v "/\" w) = (u "/\" v) "/\" w by Lm14; :: according to LATTICES:def_7 ::_thesis: NormForm A is join-absorbing let u, v be Element of (NormForm A); :: according to LATTICES:def_9 ::_thesis: u "/\" (u "\/" v) = u thus u "/\" (u "\/" v) = u by Lm16; ::_thesis: verum end; end; registration let A be set ; cluster NormForm A -> strict distributive lower-bounded ; coherence ( NormForm A is distributive & NormForm A is lower-bounded ) proof set G = NormForm A; thus NormForm A is distributive ::_thesis: NormForm A is lower-bounded proof let u, v, w be Element of (NormForm A); :: according to LATTICES:def_11 ::_thesis: u "/\" (v "\/" w) = (u "/\" v) "\/" (u "/\" w) reconsider K = u, L = v, M = w as Element of Normal_forms_on A by Def12; thus u "/\" (v "\/" w) = the L_meet of (NormForm A) . (K,( the L_join of (NormForm A) . (L,M))) .= (u "/\" v) "\/" (u "/\" w) by Lm15 ; ::_thesis: verum end; thus NormForm A is lower-bounded ::_thesis: verum proof reconsider E = {} as Element of Normal_forms_on A by Lm4; reconsider e = E as Element of (NormForm A) by Def12; take e ; :: according to LATTICES:def_13 ::_thesis: for b1 being Element of the carrier of (NormForm A) holds ( e "/\" b1 = e & b1 "/\" e = e ) let u be Element of (NormForm A); ::_thesis: ( e "/\" u = e & u "/\" e = e ) reconsider K = u as Element of Normal_forms_on A by Def12; A1: e "\/" u = mi (E \/ K) by Def12 .= u by Th42 ; then u "/\" e = e by LATTICES:def_9; hence ( e "/\" u = e & u "/\" e = e ) by A1, LATTICES:def_9; ::_thesis: verum end; end; end; theorem :: NORMFORM:56 for A being set holds {} is Element of (NormForm A) proof let A be set ; ::_thesis: {} is Element of (NormForm A) the carrier of (NormForm A) = Normal_forms_on A by Def12; hence {} is Element of (NormForm A) by Lm4; ::_thesis: verum end; theorem :: NORMFORM:57 for A being set holds Bottom (NormForm A) = {} proof let A be set ; ::_thesis: Bottom (NormForm A) = {} {} in Normal_forms_on A by Lm4; then reconsider Z = {} as Element of (NormForm A) by Def12; now__::_thesis:_for_u_being_Element_of_(NormForm_A)_holds_Z_"\/"_u_=_u let u be Element of (NormForm A); ::_thesis: Z "\/" u = u reconsider z = Z, u9 = u as Element of Normal_forms_on A by Def12; thus Z "\/" u = mi (z \/ u9) by Def12 .= u by Th42 ; ::_thesis: verum end; hence Bottom (NormForm A) = {} by LATTICE2:14; ::_thesis: verum end;