:: SETWISEO semantic presentation begin theorem Th1: :: SETWISEO:1 for x, y, z being set holds {x} c= {x,y,z} proof let x, y, z be set ; ::_thesis: {x} c= {x,y,z} {x,y,z} = {x} \/ {y,z} by ENUMSET1:2; hence {x} c= {x,y,z} by XBOOLE_1:7; ::_thesis: verum end; theorem Th2: :: SETWISEO:2 for x, y, z being set holds {x,y} c= {x,y,z} proof let x, y, z be set ; ::_thesis: {x,y} c= {x,y,z} {x,y,z} = {x,y} \/ {z} by ENUMSET1:3; hence {x,y} c= {x,y,z} by XBOOLE_1:7; ::_thesis: verum end; theorem :: SETWISEO:3 canceled; theorem :: SETWISEO:4 canceled; theorem :: SETWISEO:5 canceled; theorem Th6: :: SETWISEO:6 for X, Y being set for f being Function holds f .: (Y \ (f " X)) = (f .: Y) \ X proof let X, Y be set ; ::_thesis: for f being Function holds f .: (Y \ (f " X)) = (f .: Y) \ X let f be Function; ::_thesis: f .: (Y \ (f " X)) = (f .: Y) \ X now__::_thesis:_for_x_being_set_holds_ (_(_x_in_f_.:_(Y_\_(f_"_X))_implies_x_in_(f_.:_Y)_\_X_)_&_(_x_in_(f_.:_Y)_\_X_implies_x_in_f_.:_(Y_\_(f_"_X))_)_) let x be set ; ::_thesis: ( ( x in f .: (Y \ (f " X)) implies x in (f .: Y) \ X ) & ( x in (f .: Y) \ X implies x in f .: (Y \ (f " X)) ) ) thus ( x in f .: (Y \ (f " X)) implies x in (f .: Y) \ X ) ::_thesis: ( x in (f .: Y) \ X implies x in f .: (Y \ (f " X)) ) proof assume x in f .: (Y \ (f " X)) ; ::_thesis: x in (f .: Y) \ X then consider z being set such that A1: z in dom f and A2: z in Y \ (f " X) and A3: f . z = x by FUNCT_1:def_6; not z in f " X by A2, XBOOLE_0:def_5; then A4: not x in X by A1, A3, FUNCT_1:def_7; f . z in f .: Y by A1, A2, FUNCT_1:def_6; hence x in (f .: Y) \ X by A3, A4, XBOOLE_0:def_5; ::_thesis: verum end; assume A5: x in (f .: Y) \ X ; ::_thesis: x in f .: (Y \ (f " X)) then consider z being set such that A6: z in dom f and A7: z in Y and A8: f . z = x by FUNCT_1:def_6; not x in X by A5, XBOOLE_0:def_5; then not z in f " X by A8, FUNCT_1:def_7; then z in Y \ (f " X) by A7, XBOOLE_0:def_5; hence x in f .: (Y \ (f " X)) by A6, A8, FUNCT_1:def_6; ::_thesis: verum end; hence f .: (Y \ (f " X)) = (f .: Y) \ X by TARSKI:1; ::_thesis: verum end; theorem Th7: :: SETWISEO:7 for Y, X being non empty set for f being Function of X,Y for x being Element of X holds x in f " {(f . x)} proof let Y, X be non empty set ; ::_thesis: for f being Function of X,Y for x being Element of X holds x in f " {(f . x)} let f be Function of X,Y; ::_thesis: for x being Element of X holds x in f " {(f . x)} let x be Element of X; ::_thesis: x in f " {(f . x)} f . x in {(f . x)} by TARSKI:def_1; hence x in f " {(f . x)} by FUNCT_2:38; ::_thesis: verum end; theorem Th8: :: SETWISEO:8 for Y, X being non empty set for f being Function of X,Y for x being Element of X holds Im (f,x) = {(f . x)} proof let Y, X be non empty set ; ::_thesis: for f being Function of X,Y for x being Element of X holds Im (f,x) = {(f . x)} let f be Function of X,Y; ::_thesis: for x being Element of X holds Im (f,x) = {(f . x)} let x be Element of X; ::_thesis: Im (f,x) = {(f . x)} for y being set holds ( y in f .: {x} iff y = f . x ) proof let y be set ; ::_thesis: ( y in f .: {x} iff y = f . x ) thus ( y in f .: {x} implies y = f . x ) ::_thesis: ( y = f . x implies y in f .: {x} ) proof assume y in f .: {x} ; ::_thesis: y = f . x then ex z being set st ( z in dom f & z in {x} & f . z = y ) by FUNCT_1:def_6; hence y = f . x by TARSKI:def_1; ::_thesis: verum end; x in {x} by TARSKI:def_1; hence ( y = f . x implies y in f .: {x} ) by FUNCT_2:35; ::_thesis: verum end; hence Im (f,x) = {(f . x)} by TARSKI:def_1; ::_thesis: verum end; theorem Th9: :: SETWISEO:9 for X being non empty set for B being Element of Fin X for x being set st x in B holds x is Element of X proof let X be non empty set ; ::_thesis: for B being Element of Fin X for x being set st x in B holds x is Element of X let B be Element of Fin X; ::_thesis: for x being set st x in B holds x is Element of X A1: B c= X by FINSUB_1:def_5; let x be set ; ::_thesis: ( x in B implies x is Element of X ) assume x in B ; ::_thesis: x is Element of X hence x is Element of X by A1; ::_thesis: verum end; theorem :: SETWISEO:10 for X, Y being non empty set for A being Element of Fin X for B being set for f being Function of X,Y st ( for x being Element of X st x in A holds f . x in B ) holds f .: A c= B proof let X, Y be non empty set ; ::_thesis: for A being Element of Fin X for B being set for f being Function of X,Y st ( for x being Element of X st x in A holds f . x in B ) holds f .: A c= B let A be Element of Fin X; ::_thesis: for B being set for f being Function of X,Y st ( for x being Element of X st x in A holds f . x in B ) holds f .: A c= B let B be set ; ::_thesis: for f being Function of X,Y st ( for x being Element of X st x in A holds f . x in B ) holds f .: A c= B let f be Function of X,Y; ::_thesis: ( ( for x being Element of X st x in A holds f . x in B ) implies f .: A c= B ) assume A1: for x being Element of X st x in A holds f . x in B ; ::_thesis: f .: A c= B let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f .: A or x in B ) assume x in f .: A ; ::_thesis: x in B 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_6; reconsider y = y as Element of X by A2, Th9; x = f . y by A3; hence x in B by A1, A2; ::_thesis: verum end; theorem Th11: :: SETWISEO:11 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 ; ::_thesis: for B being Element of Fin X for A being set st A c= B holds A is Element of Fin X let B be Element of Fin X; ::_thesis: for A being set st A c= B holds A is Element of Fin X let A be set ; ::_thesis: ( A c= B implies A is Element of Fin X ) assume A1: A c= B ; ::_thesis: A is Element of Fin X B c= X by FINSUB_1:def_5; then A c= X by A1, XBOOLE_1:1; hence A is Element of Fin X by A1, FINSUB_1:def_5; ::_thesis: verum end; Lm1: for X, Y being non empty set for f being Function of X,Y for A being Element of Fin X holds f .: A is Element of Fin Y by FINSUB_1:def_5; theorem Th12: :: SETWISEO:12 for X being non empty set for B being Element of Fin X st B <> {} holds ex x being Element of X st x in B proof let X be non empty set ; ::_thesis: for B being Element of Fin X st B <> {} holds ex x being Element of X st x in B let B be Element of Fin X; ::_thesis: ( B <> {} implies ex x being Element of X st x in B ) set x = the Element of B; assume A1: B <> {} ; ::_thesis: ex x being Element of X st x in B then reconsider x = the Element of B as Element of X by Th9; take x ; ::_thesis: x in B thus x in B by A1; ::_thesis: verum end; theorem Th13: :: SETWISEO:13 for Y, X being non empty set for f being Function of X,Y for A being Element of Fin X st f .: A = {} holds A = {} proof let Y, X be non empty set ; ::_thesis: for f being Function of X,Y for A being Element of Fin X st f .: A = {} holds A = {} let f be Function of X,Y; ::_thesis: for A being Element of Fin X st f .: A = {} holds A = {} let A be Element of Fin X; ::_thesis: ( f .: A = {} implies A = {} ) assume A1: f .: A = {} ; ::_thesis: A = {} assume A <> {} ; ::_thesis: contradiction then consider x being Element of X such that A2: x in A by Th12; f . x in f .: A by A2, FUNCT_2:35; hence contradiction by A1; ::_thesis: verum end; registration let X be set ; cluster empty finite for Element of Fin X; existence ex b1 being Element of Fin X st b1 is empty proof {} is Element of Fin X by FINSUB_1:7; hence ex b1 being Element of Fin X st b1 is empty ; ::_thesis: verum end; end; definition let X be set ; func {}. X -> empty Element of Fin X equals :: SETWISEO:def 1 {} ; coherence {} is empty Element of Fin X by FINSUB_1:7; end; :: deftheorem defines {}. SETWISEO:def_1_:_ for X being set holds {}. X = {} ; scheme :: SETWISEO:sch 1 FinSubFuncEx{ F1() -> non empty set , F2() -> Element of Fin F1(), P1[ set , set ] } : ex f being Function of F1(),(Fin F1()) st for b, a being Element of F1() holds ( a in f . b iff ( a in F2() & P1[a,b] ) ) proof defpred S1[ set , Element of Fin F1()] means for a being Element of F1() holds ( a in \$2 iff ( a in F2() & P1[a,\$1] ) ); A1: now__::_thesis:_for_x_being_Element_of_F1()_ex_y9_being_Element_of_Fin_F1()_st_S1[x,y9] reconsider B = F2() as Subset of F1() by FINSUB_1:def_5; let x be Element of F1(); ::_thesis: ex y9 being Element of Fin F1() st S1[x,y9] defpred S2[ set ] means ( \$1 in F2() & P1[\$1,x] ); consider y being Subset of F1() such that A2: for a being Element of F1() holds ( a in y iff S2[a] ) from SUBSET_1:sch_3(); for x being Element of F1() st x in y holds x in B by A2; then y c= F2() by SUBSET_1:2; then reconsider y = y as Element of Fin F1() by FINSUB_1:def_5; take y9 = y; ::_thesis: S1[x,y9] thus S1[x,y9] by A2; ::_thesis: verum end; thus ex f being Function of F1(),(Fin F1()) st for x being Element of F1() holds S1[x,f . x] from FUNCT_2:sch_3(A1); ::_thesis: verum end; definition let X be non empty set ; let F be BinOp of X; attrF is having_a_unity means :Def2: :: SETWISEO:def 2 ex x being Element of X st x is_a_unity_wrt F; end; :: deftheorem Def2 defines having_a_unity SETWISEO:def_2_:_ for X being non empty set for F being BinOp of X holds ( F is having_a_unity iff ex x being Element of X st x is_a_unity_wrt F ); theorem Th14: :: SETWISEO:14 for X being non empty set for F being BinOp of X holds ( F is having_a_unity iff the_unity_wrt F is_a_unity_wrt F ) proof let X be non empty set ; ::_thesis: for F being BinOp of X holds ( F is having_a_unity iff the_unity_wrt F is_a_unity_wrt F ) let F be BinOp of X; ::_thesis: ( F is having_a_unity iff the_unity_wrt F is_a_unity_wrt F ) thus ( F is having_a_unity implies the_unity_wrt F is_a_unity_wrt F ) ::_thesis: ( the_unity_wrt F is_a_unity_wrt F implies F is having_a_unity ) proof assume F is having_a_unity ; ::_thesis: the_unity_wrt F is_a_unity_wrt F 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; ::_thesis: verum end; thus ( the_unity_wrt F is_a_unity_wrt F implies F is having_a_unity ) by Def2; ::_thesis: verum end; theorem Th15: :: SETWISEO:15 for X being non empty set for F being BinOp of X st F is having_a_unity holds 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 ; ::_thesis: for F being BinOp of X st F is having_a_unity holds for x being Element of X holds ( F . ((the_unity_wrt F),x) = x & F . (x,(the_unity_wrt F)) = x ) let F be BinOp of X; ::_thesis: ( F is having_a_unity implies for x being Element of X holds ( F . ((the_unity_wrt F),x) = x & F . (x,(the_unity_wrt F)) = x ) ) assume F is having_a_unity ; ::_thesis: for x being Element of X holds ( F . ((the_unity_wrt F),x) = x & F . (x,(the_unity_wrt F)) = x ) then A1: the_unity_wrt F is_a_unity_wrt F by Th14; let x be Element of X; ::_thesis: ( F . ((the_unity_wrt F),x) = x & F . (x,(the_unity_wrt F)) = x ) thus ( F . ((the_unity_wrt F),x) = x & F . (x,(the_unity_wrt F)) = x ) by A1, BINOP_1:3; ::_thesis: verum end; registration let X be non empty set ; cluster non empty finite for Element of Fin X; existence not for b1 being Element of Fin X holds b1 is empty proof set x = the Element of X; { the Element of X} is Subset of X by SUBSET_1:41; then { the Element of X} is Element of Fin X by FINSUB_1:def_5; hence not for b1 being Element of Fin X holds b1 is empty ; ::_thesis: verum end; end; notation let X be non empty set ; let x be Element of X; synonym {.x.} for {X}; let y be Element of X; synonym {.x,y.} for {X,x}; let z be Element of X; synonym {.x,y,z.} for {X,x,y}; end; definition let X be non empty set ; let x be Element of X; :: original: {. redefine func{.x.} -> Element of Fin X; coherence {..} is Element of Fin X proof {x} is Subset of X by SUBSET_1:41; hence {..} is Element of Fin X by FINSUB_1:def_5; ::_thesis: verum end; let y be Element of X; :: original: {. redefine func{.x,y.} -> Element of Fin X; coherence {.y,.} is Element of Fin X proof {x,y} is Subset of X by SUBSET_1:34; hence {.y,.} is Element of Fin X by FINSUB_1:def_5; ::_thesis: verum end; let z be Element of X; :: original: {. redefine func{.x,y,z.} -> Element of Fin X; coherence {.y,z,.} is Element of Fin X proof {x,y,z} is Subset of X by SUBSET_1:35; hence {.y,z,.} is Element of Fin X by FINSUB_1:def_5; ::_thesis: verum end; end; definition let X be set ; let A, B be Element of Fin X; :: original: \/ redefine funcA \/ B -> Element of Fin X; coherence A \/ B is Element of Fin X by FINSUB_1:1; end; definition let X be set ; let A, B be Element of Fin X; :: original: \ redefine funcA \ B -> Element of Fin X; coherence A \ B is Element of Fin X by FINSUB_1:1; end; scheme :: SETWISEO:sch 2 FinSubInd1{ F1() -> non empty set , P1[ set ] } : for B being Element of Fin F1() holds P1[B] provided A1: P1[ {}. F1()] and A2: for B9 being Element of Fin F1() for b being Element of F1() st P1[B9] & not b in B9 holds P1[B9 \/ {b}] proof defpred S1[ set ] means ex B9 being Element of Fin F1() st ( B9 = \$1 & P1[B9] ); let B be Element of Fin F1(); ::_thesis: P1[B] A3: for x, A being set st x in B & A c= B & S1[A] holds S1[A \/ {x}] proof let x, A be set ; ::_thesis: ( x in B & A c= B & S1[A] implies S1[A \/ {x}] ) assume that A4: x in B and A5: A c= B and A6: ex B9 being Element of Fin F1() st ( B9 = A & P1[B9] ) ; ::_thesis: S1[A \/ {x}] reconsider x9 = x as Element of F1() by A4, Th9; reconsider A9 = A as Element of Fin F1() by A5, Th11; take A9 \/ {.x9.} ; ::_thesis: ( A9 \/ {.x9.} = A \/ {x} & P1[A9 \/ {.x9.}] ) thus A9 \/ {.x9.} = A \/ {x} ; ::_thesis: P1[A9 \/ {.x9.}] thus P1[A9 \/ {x9}] by A2, A6, ZFMISC_1:40; ::_thesis: verum end; A7: B is finite ; A8: S1[ {} ] by A1; S1[B] from FINSET_1:sch_2(A7, A8, A3); hence P1[B] ; ::_thesis: verum end; scheme :: SETWISEO:sch 3 FinSubInd2{ F1() -> non empty set , P1[ Element of Fin F1()] } : for B being non empty Element of Fin F1() holds P1[B] provided A1: for x being Element of F1() holds P1[{.x.}] and A2: for B1, B2 being non empty Element of Fin F1() st P1[B1] & P1[B2] holds P1[B1 \/ B2] proof defpred S1[ set ] means ( \$1 <> {} implies ex B9 being Element of Fin F1() st ( B9 = \$1 & P1[B9] ) ); let B be non empty Element of Fin F1(); ::_thesis: P1[B] A3: for x, A being set st x in B & A c= B & S1[A] holds S1[A \/ {x}] proof let x, A be set ; ::_thesis: ( x in B & A c= B & S1[A] implies S1[A \/ {x}] ) assume that A4: x in B and A5: A c= B and A6: ( A <> {} implies ex B9 being Element of Fin F1() st ( B9 = A & P1[B9] ) ) and A \/ {x} <> {} ; ::_thesis: ex B9 being Element of Fin F1() st ( B9 = A \/ {x} & P1[B9] ) reconsider x9 = x as Element of F1() by A4, Th9; reconsider A9 = A as Element of Fin F1() by A5, Th11; take A9 \/ {.x9.} ; ::_thesis: ( A9 \/ {.x9.} = A \/ {x} & P1[A9 \/ {.x9.}] ) thus A9 \/ {.x9.} = A \/ {x} ; ::_thesis: P1[A9 \/ {.x9.}] A7: P1[{.x9.}] by A1; percases ( A = {} or A <> {} ) ; suppose A = {} ; ::_thesis: P1[A9 \/ {.x9.}] hence P1[A9 \/ {.x9.}] by A1; ::_thesis: verum end; suppose A <> {} ; ::_thesis: P1[A9 \/ {.x9.}] hence P1[A9 \/ {.x9.}] by A2, A6, A7; ::_thesis: verum end; end; end; A8: S1[ {} ] ; A9: B is finite ; S1[B] from FINSET_1:sch_2(A9, A8, A3); hence P1[B] ; ::_thesis: verum end; scheme :: SETWISEO:sch 4 FinSubInd3{ F1() -> non empty set , P1[ set ] } : for B being Element of Fin F1() holds P1[B] provided A1: P1[ {}. F1()] and A2: for B9 being Element of Fin F1() for b being Element of F1() st P1[B9] holds P1[B9 \/ {b}] proof A3: for B9 being Element of Fin F1() for b being Element of F1() st P1[B9] & not b in B9 holds P1[B9 \/ {b}] by A2; A4: P1[ {}. F1()] by A1; thus for B being Element of Fin F1() holds P1[B] from SETWISEO:sch_2(A4, A3); ::_thesis: verum 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 is having_a_unity ) and A2: F is commutative and A3: F is associative ; funcF \$\$ (B,f) -> Element of Y means :Def3: :: SETWISEO:def 3 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B \ B9 holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ); existence ex b1 being Element of Y ex G being Function of (Fin X),Y st ( b1 = 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B \ B9 holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) proof defpred S1[ 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 B9 being Element of Fin X st B9 c= \$1 & B9 <> {} holds for x being Element of X st x in \$1 \ B9 holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ); A4: for B9 being Element of Fin X for b being Element of X st S1[B9] & not b in B9 holds S1[B9 \/ {b}] proof let B be Element of Fin X; ::_thesis: for b being Element of X st S1[B] & not b in B holds S1[B \/ {b}] let x be Element of X; ::_thesis: ( S1[B] & not x in B implies S1[B \/ {x}] ) given G being Function of (Fin X),Y such that A5: for e being Element of Y st e is_a_unity_wrt F holds G . {} = e and A6: for x being Element of X holds G . {x} = f . x and A7: for B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B \ B9 holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ; ::_thesis: ( x in B or S1[B \/ {x}] ) assume A8: not x in B ; ::_thesis: S1[B \/ {x}] 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 B9 being Element of Fin X st B9 c= B \/ {x} & B9 <> {} holds for x9 being Element of X st x9 in (B \/ {x}) \ B9 holds G . (B9 \/ {x9}) = F . ((G . B9),(f . x9)) ) ) ::_thesis: verum proof defpred S2[ 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)) ) & ( ( for C being Element of Fin X holds ( not C <> {} or not C c= B or not \$1 = C \/ {.x.} ) ) implies \$2 = G . \$1 ) ); A9: now__::_thesis:_for_B9_being_Element_of_Fin_X_ex_y_being_Element_of_Y_st_S2[B9,y] let B9 be Element of Fin X; ::_thesis: ex y being Element of Y st S2[B9,y] thus ex y being Element of Y st S2[B9,y] ::_thesis: verum proof A10: now__::_thesis:_(_ex_C_being_Element_of_Fin_X_st_ (_C_<>_{}_&_C_c=_B_&_B9_=_C_\/_{x}_)_implies_ex_y_being_Element_of_Y_ex_y_being_Element_of_Y_st_S2[B9,y]_) given C being Element of Fin X such that A11: C <> {} and A12: C c= B and A13: B9 = C \/ {x} ; ::_thesis: ex y being Element of Y ex y being Element of Y st S2[B9,y] take y = F . ((G . C),(f . x)); ::_thesis: ex y being Element of Y st S2[B9,y] for C being Element of Fin X st C <> {} & C c= B & B9 = C \/ {x} holds y = F . ((G . C),(f . x)) proof not x in C by A8, A12; then A14: C c= B9 \ {x} by A13, XBOOLE_1:7, ZFMISC_1:34; B9 \ {x} = C \ {x} by A13, XBOOLE_1:40; then A15: B9 \ {x} = C by A14, XBOOLE_0:def_10; let C1 be Element of Fin X; ::_thesis: ( C1 <> {} & C1 c= B & B9 = C1 \/ {x} implies y = F . ((G . C1),(f . x)) ) assume that C1 <> {} and A16: C1 c= B and A17: B9 = C1 \/ {x} ; ::_thesis: y = F . ((G . C1),(f . x)) not x in C1 by A8, A16; then A18: C1 c= B9 \ {x} by A17, XBOOLE_1:7, ZFMISC_1:34; B9 \ {x} = C1 \ {x} by A17, XBOOLE_1:40; hence y = F . ((G . C1),(f . x)) by A18, A15, XBOOLE_0:def_10; ::_thesis: verum end; hence ex y being Element of Y st S2[B9,y] by A11, A12, A13; ::_thesis: verum end; now__::_thesis:_(_(_for_C_being_Element_of_Fin_X_holds_ (_not_C_<>_{}_or_not_C_c=_B_or_not_B9_=_C_\/_{x}_)_)_implies_ex_y_being_Element_of_Y_st_ (_(_for_C_being_Element_of_Fin_X_st_C_<>_{}_&_C_c=_B_&_B9_=_C_\/_{x}_holds_ y_=_F_._((G_._C),(f_._x))_)_&_(_(_for_C_being_Element_of_Fin_X_holds_ (_not_C_<>_{}_or_not_C_c=_B_or_not_B9_=_C_\/_{x}_)_)_implies_y_=_G_._B9_)_)_) assume A19: for C being Element of Fin X holds ( not C <> {} or not C c= B or not B9 = C \/ {x} ) ; ::_thesis: ex y being Element of Y st ( ( for C being Element of Fin X st C <> {} & C c= B & B9 = C \/ {x} holds y = F . ((G . C),(f . x)) ) & ( ( for C being Element of Fin X holds ( not C <> {} or not C c= B or not B9 = C \/ {x} ) ) implies y = G . B9 ) ) take y = G . B9; ::_thesis: ( ( for C being Element of Fin X st C <> {} & C c= B & B9 = C \/ {x} holds y = F . ((G . C),(f . x)) ) & ( ( for C being Element of Fin X holds ( not C <> {} or not C c= B or not B9 = C \/ {x} ) ) implies y = G . B9 ) ) thus for C being Element of Fin X st C <> {} & C c= B & B9 = C \/ {x} holds y = F . ((G . C),(f . x)) by A19; ::_thesis: ( ( for C being Element of Fin X holds ( not C <> {} or not C c= B or not B9 = C \/ {x} ) ) implies y = G . B9 ) thus ( ( for C being Element of Fin X holds ( not C <> {} or not C c= B or not B9 = C \/ {x} ) ) implies y = G . B9 ) ; ::_thesis: verum end; hence ex y being Element of Y st S2[B9,y] by A10; ::_thesis: verum end; end; consider H being Function of (Fin X),Y such that A20: for B9 being Element of Fin X holds S2[B9,H . B9] from FUNCT_2:sch_3(A9); take J = H; ::_thesis: ( ( for e being Element of Y st e is_a_unity_wrt F holds J . {} = e ) & ( for x being Element of X holds J . {x} = f . x ) & ( for B9 being Element of Fin X st B9 c= B \/ {x} & B9 <> {} holds for x9 being Element of X st x9 in (B \/ {x}) \ B9 holds J . (B9 \/ {x9}) = F . ((J . B9),(f . x9)) ) ) now__::_thesis:_for_C_being_Element_of_Fin_X_holds_ (_not_C_<>_{}_or_not_C_c=_B_or_not_{x}_=_C_\/_{x}_) given C being Element of Fin X such that A21: C <> {} and A22: C c= B and A23: {x} = C \/ {x} ; ::_thesis: contradiction C = {x} by A21, ZFMISC_1:33, A23, XBOOLE_1:7; then x in C by TARSKI:def_1; hence contradiction by A8, A22; ::_thesis: verum end; then A24: J . {x} = G . {.x.} by A20; thus for e being Element of Y st e is_a_unity_wrt F holds J . {} = e ::_thesis: ( ( for x being Element of X holds J . {x} = f . x ) & ( for B9 being Element of Fin X st B9 c= B \/ {x} & B9 <> {} holds for x9 being Element of X st x9 in (B \/ {x}) \ B9 holds J . (B9 \/ {x9}) = F . ((J . B9),(f . x9)) ) ) proof reconsider E = {} as Element of Fin X by FINSUB_1:7; for C being Element of Fin X holds ( not C <> {} or not C c= B or not E = C \/ {x} ) ; then J . E = G . E by A20; hence for e being Element of Y st e is_a_unity_wrt F holds J . {} = e by A5; ::_thesis: verum end; thus for x being Element of X holds J . {x} = f . x ::_thesis: for B9 being Element of Fin X st B9 c= B \/ {x} & B9 <> {} holds for x9 being Element of X st x9 in (B \/ {x}) \ B9 holds J . (B9 \/ {x9}) = F . ((J . B9),(f . x9)) proof let x9 be Element of X; ::_thesis: J . {x9} = f . x9 now__::_thesis:_for_C_being_Element_of_Fin_X_holds_ (_not_C_<>_{}_or_not_C_c=_B_or_not_{x9}_=_C_\/_{x}_) given C being Element of Fin X such that A25: C <> {} and A26: C c= B and A27: {x9} = C \/ {x} ; ::_thesis: contradiction A28: C = {x9} by A25, ZFMISC_1:33, A27, XBOOLE_1:7; x = x9 by A27, XBOOLE_1:7, ZFMISC_1:18; then x in C by A28, TARSKI:def_1; hence contradiction by A8, A26; ::_thesis: verum end; hence J . {x9} = G . {.x9.} by A20 .= f . x9 by A6 ; ::_thesis: verum end; let B9 be Element of Fin X; ::_thesis: ( B9 c= B \/ {x} & B9 <> {} implies for x9 being Element of X st x9 in (B \/ {x}) \ B9 holds J . (B9 \/ {x9}) = F . ((J . B9),(f . x9)) ) assume that A29: B9 c= B \/ {x} and A30: B9 <> {} ; ::_thesis: for x9 being Element of X st x9 in (B \/ {x}) \ B9 holds J . (B9 \/ {x9}) = F . ((J . B9),(f . x9)) let x9 be Element of X; ::_thesis: ( x9 in (B \/ {x}) \ B9 implies J . (B9 \/ {x9}) = F . ((J . B9),(f . x9)) ) assume A31: x9 in (B \/ {x}) \ B9 ; ::_thesis: J . (B9 \/ {x9}) = F . ((J . B9),(f . x9)) then A32: not x9 in B9 by XBOOLE_0:def_5; percases ( x in B9 or not x in B9 ) ; supposeA33: x in B9 ; ::_thesis: J . (B9 \/ {x9}) = F . ((J . B9),(f . x9)) then A34: x9 in B by A31, A32, ZFMISC_1:136; percases ( B9 = {x} or B9 <> {x} ) ; supposeA36: B9 = {x} ; ::_thesis: J . (B9 \/ {x9}) = F . ((J . B9),(f . x9)) hence J . (B9 \/ {.x9.}) = F . ((G . {.x9.}),(f . x)) by A20, ZFMISC_1:31, A34 .= F . ((f . x9),(f . x)) by A6 .= F . ((f . x),(f . x9)) by A2, BINOP_1:def_2 .= F . ((J . B9),(f . x9)) by A6, A24, A36 ; ::_thesis: verum end; suppose B9 <> {x} ; ::_thesis: J . (B9 \/ {x9}) = F . ((J . B9),(f . x9)) then not B9 c= {x} by A30, ZFMISC_1:33; then A37: B9 \ {x} <> {} by XBOOLE_1:37; set C = (B9 \ {.x.}) \/ {.x9.}; not x9 in B9 \ {x} by A31, XBOOLE_0:def_5; then A38: x9 in B \ (B9 \ {x}) by A34, XBOOLE_0:def_5; B9 \ {x} c= B by A29, XBOOLE_1:43; then A39: (B9 \ {.x.}) \/ {.x9.} c= B by A33, ZFMISC_1:137, A31, A32, ZFMISC_1:136; B9 \/ {.x9.} = (B9 \/ {x}) \/ {x9} by A33, ZFMISC_1:40 .= ((B9 \ {x}) \/ {x}) \/ {x9} by XBOOLE_1:39 .= ((B9 \ {.x.}) \/ {.x9.}) \/ {.x.} by XBOOLE_1:4 ; hence J . (B9 \/ {.x9.}) = F . ((G . ((B9 \ {.x.}) \/ {.x9.})),(f . x)) by A20, A39 .= F . ((F . ((G . (B9 \ {.x.})),(f . x9))),(f . x)) by A7, A29, A37, A38, XBOOLE_1:43 .= F . ((G . (B9 \ {.x.})),(F . ((f . x9),(f . x)))) by A3, BINOP_1:def_3 .= F . ((G . (B9 \ {x})),(F . ((f . x),(f . x9)))) by A2, BINOP_1:def_2 .= F . ((F . ((G . (B9 \ {.x.})),(f . x))),(f . x9)) by A3, BINOP_1:def_3 .= F . ((J . ((B9 \ {.x.}) \/ {.x.})),(f . x9)) by A20, A29, A37, XBOOLE_1:43 .= F . ((J . (B9 \/ {x})),(f . x9)) by XBOOLE_1:39 .= F . ((J . B9),(f . x9)) by A33, ZFMISC_1:40 ; ::_thesis: verum end; end; end; supposeA40: not x in B9 ; ::_thesis: J . (B9 \/ {x9}) = F . ((J . B9),(f . x9)) then A41: B9 c= B by A29, ZFMISC_1:135; A42: for C being Element of Fin X holds ( not C <> {} or not C c= B or not B9 = C \/ {x} ) by A40, ZFMISC_1:136; percases ( x <> x9 or x = x9 ) ; supposeA43: x <> x9 ; ::_thesis: J . (B9 \/ {x9}) = F . ((J . B9),(f . x9)) then x9 in B by A31, ZFMISC_1:136; then A44: x9 in B \ B9 by A32, XBOOLE_0:def_5; not x in B9 \/ {x9} by A40, A43, ZFMISC_1:136; then for C being Element of Fin X holds ( not C <> {} or not C c= B or not B9 \/ {x9} = C \/ {x} ) by ZFMISC_1:136; hence J . (B9 \/ {.x9.}) = G . (B9 \/ {.x9.}) by A20 .= F . ((G . B9),(f . x9)) by A7, A30, A41, A44 .= F . ((J . B9),(f . x9)) by A20, A42 ; ::_thesis: verum end; suppose x = x9 ; ::_thesis: J . (B9 \/ {x9}) = F . ((J . B9),(f . x9)) hence J . (B9 \/ {.x9.}) = F . ((G . B9),(f . x9)) by A20, A29, A30, A40, ZFMISC_1:135 .= F . ((J . B9),(f . x9)) by A20, A42 ; ::_thesis: verum end; end; end; end; end; end; A45: S1[ {}. X] proof consider e being Element of Y such that A46: ( ex e being Element of Y st e is_a_unity_wrt F implies e = the_unity_wrt F ) ; defpred S2[ set , set ] means ( ( for x9 being Element of X st \$1 = {x9} holds \$2 = f . x9 ) & ( ( for x9 being Element of X holds not \$1 = {x9} ) implies \$2 = e ) ); A47: now__::_thesis:_for_x_being_Element_of_Fin_X_ex_y_being_Element_of_Y_st_S2[x,y] let x be Element of Fin X; ::_thesis: ex y being Element of Y st S2[x,y] A48: now__::_thesis:_(_ex_x9_being_Element_of_X_st_x_=_{x9}_implies_ex_y_being_Element_of_Y_st_ (_(_for_x9_being_Element_of_X_st_x_=_{x9}_holds_ y_=_f_._x9_)_&_(_(_for_x9_being_Element_of_X_holds_not_x_=_{x9}_)_implies_y_=_e_)_)_) given x9 being Element of X such that A49: x = {x9} ; ::_thesis: ex y being Element of Y st ( ( for x9 being Element of X st x = {x9} holds y = f . x9 ) & ( ( for x9 being Element of X holds not x = {x9} ) implies y = e ) ) take y = f . x9; ::_thesis: ( ( for x9 being Element of X st x = {x9} holds y = f . x9 ) & ( ( for x9 being Element of X holds not x = {x9} ) implies y = e ) ) thus for x9 being Element of X st x = {x9} holds y = f . x9 by A49, ZFMISC_1:3; ::_thesis: ( ( for x9 being Element of X holds not x = {x9} ) implies y = e ) thus ( ( for x9 being Element of X holds not x = {x9} ) implies y = e ) by A49; ::_thesis: verum end; now__::_thesis:_(_(_for_x9_being_Element_of_X_holds_not_x_=_{x9}_)_implies_ex_y_being_Element_of_Y_st_ (_(_for_x9_being_Element_of_X_st_x_=_{x9}_holds_ y_=_f_._x9_)_&_(_(_for_x9_being_Element_of_X_holds_not_x_=_{x9}_)_implies_y_=_e_)_)_) assume A50: for x9 being Element of X holds not x = {x9} ; ::_thesis: ex y being Element of Y st ( ( for x9 being Element of X st x = {x9} holds y = f . x9 ) & ( ( for x9 being Element of X holds not x = {x9} ) implies y = e ) ) take y = e; ::_thesis: ( ( for x9 being Element of X st x = {x9} holds y = f . x9 ) & ( ( for x9 being Element of X holds not x = {x9} ) implies y = e ) ) thus ( ( for x9 being Element of X st x = {x9} holds y = f . x9 ) & ( ( for x9 being Element of X holds not x = {x9} ) implies y = e ) ) by A50; ::_thesis: verum end; hence ex y being Element of Y st S2[x,y] by A48; ::_thesis: verum end; consider G9 being Function of (Fin X),Y such that A51: for B9 being Element of Fin X holds S2[B9,G9 . B9] from FUNCT_2:sch_3(A47); take G = G9; ::_thesis: ( ( 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 B9 being Element of Fin X st B9 c= {}. X & B9 <> {} holds for x being Element of X st x in ({}. X) \ B9 holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) thus for e being Element of Y st e is_a_unity_wrt F holds G . {} = e ::_thesis: ( ( for x being Element of X holds G . {x} = f . x ) & ( for B9 being Element of Fin X st B9 c= {}. X & B9 <> {} holds for x being Element of X st x in ({}. X) \ B9 holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) proof reconsider E = {} as Element of Fin X by FINSUB_1:7; let e9 be Element of Y; ::_thesis: ( e9 is_a_unity_wrt F implies G . {} = e9 ) assume A52: e9 is_a_unity_wrt F ; ::_thesis: G . {} = e9 for x9 being Element of X holds not E = {x9} ; hence G . {} = e by A51 .= e9 by A46, A52, BINOP_1:def_8 ; ::_thesis: verum end; thus for x being Element of X holds G . {.x.} = f . x by A51; ::_thesis: for B9 being Element of Fin X st B9 c= {}. X & B9 <> {} holds for x being Element of X st x in ({}. X) \ B9 holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) thus for B9 being Element of Fin X st B9 c= {}. X & B9 <> {} holds for x being Element of X st x in ({}. X) \ B9 holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ; ::_thesis: verum end; for B being Element of Fin X holds S1[B] from SETWISEO:sch_2(A45, A4); then consider G being Function of (Fin X),Y such that A53: ( ( 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B \ B9 holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) ; take G . B ; ::_thesis: ex G being Function of (Fin X),Y st ( G . B = 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B \ B9 holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) take G ; ::_thesis: ( G . B = 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B \ B9 holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) thus ( G . B = 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B \ B9 holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) by A53; ::_thesis: verum end; uniqueness for b1, b2 being Element of Y st ex G being Function of (Fin X),Y st ( b1 = 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B \ B9 holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) & ex G being Function of (Fin X),Y st ( b2 = 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B \ B9 holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) holds b1 = b2 proof let x, y be Element of Y; ::_thesis: ( ex G being Function of (Fin X),Y st ( x = 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B \ B9 holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) & ex G being Function of (Fin X),Y st ( y = 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B \ B9 holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) implies x = y ) given G1 being Function of (Fin X),Y such that A54: x = G1 . B and A55: for e being Element of Y st e is_a_unity_wrt F holds G1 . {} = e and A56: for x being Element of X holds G1 . {x} = f . x and A57: for B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B \ B9 holds G1 . (B9 \/ {x}) = F . ((G1 . B9),(f . x)) ; ::_thesis: ( for G being Function of (Fin X),Y holds ( not y = G . B or ex e being Element of Y st ( e is_a_unity_wrt F & not G . {} = e ) or ex x being Element of X st not G . {x} = f . x or ex B9 being Element of Fin X st ( B9 c= B & B9 <> {} & ex x being Element of X st ( x in B \ B9 & not G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) ) or x = y ) given G2 being Function of (Fin X),Y such that A58: y = G2 . B and A59: for e being Element of Y st e is_a_unity_wrt F holds G2 . {} = e and A60: for x being Element of X holds G2 . {x} = f . x and A61: for B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B \ B9 holds G2 . (B9 \/ {x}) = F . ((G2 . B9),(f . x)) ; ::_thesis: x = y percases ( B = {} or B <> {} ) ; supposeA62: B = {} ; ::_thesis: x = y thus x = the_unity_wrt F by A54, A55, A62, A1, Th14 .= y by A58, A59, A62, A1, Th14 ; ::_thesis: verum end; supposeA64: B <> {} ; ::_thesis: x = y defpred S1[ set ] means ( \$1 c= B & \$1 <> {} implies G1 . \$1 = G2 . \$1 ); A65: for B9 being Element of Fin X for b being Element of X st S1[B9] & not b in B9 holds S1[B9 \/ {b}] proof let B9 be Element of Fin X; ::_thesis: for b being Element of X st S1[B9] & not b in B9 holds S1[B9 \/ {b}] let x be Element of X; ::_thesis: ( S1[B9] & not x in B9 implies S1[B9 \/ {x}] ) assume A66: ( B9 c= B & B9 <> {} implies G1 . B9 = G2 . B9 ) ; ::_thesis: ( x in B9 or S1[B9 \/ {x}] ) assume A67: not x in B9 ; ::_thesis: S1[B9 \/ {x}] assume A68: B9 \/ {x} c= B ; ::_thesis: ( not B9 \/ {x} <> {} or G1 . (B9 \/ {x}) = G2 . (B9 \/ {x}) ) then A69: B9 c= B by ZFMISC_1:137; assume B9 \/ {x} <> {} ; ::_thesis: G1 . (B9 \/ {x}) = G2 . (B9 \/ {x}) x in B by A68, ZFMISC_1:137; then A70: x in B \ B9 by A67, XBOOLE_0:def_5; percases ( B9 = {} or B9 <> {} ) ; supposeA71: B9 = {} ; ::_thesis: G1 . (B9 \/ {x}) = G2 . (B9 \/ {x}) hence G1 . (B9 \/ {x}) = f . x by A56 .= G2 . (B9 \/ {x}) by A60, A71 ; ::_thesis: verum end; supposeA72: B9 <> {} ; ::_thesis: G1 . (B9 \/ {x}) = G2 . (B9 \/ {x}) hence G1 . (B9 \/ {x}) = F . ((G1 . B9),(f . x)) by A57, A69, A70 .= G2 . (B9 \/ {x}) by A61, A66, A69, A70, A72 ; ::_thesis: verum end; end; end; A73: S1[ {}. X] ; for B9 being Element of Fin X holds S1[B9] from SETWISEO:sch_2(A73, A65); hence x = y by A54, A58, A64; ::_thesis: verum end; end; end; end; :: deftheorem Def3 defines \$\$ SETWISEO:def_3_:_ 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 is having_a_unity ) & F is commutative & F is associative holds for b6 being Element of Y holds ( b6 = F \$\$ (B,f) iff ex G being Function of (Fin X),Y st ( b6 = 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B \ B9 holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) ); theorem Th16: :: SETWISEO:16 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 is having_a_unity ) & F is idempotent & F is commutative & F is associative holds 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) ) proof let X, Y be non empty set ; ::_thesis: for F being BinOp of Y for B being Element of Fin X for f being Function of X,Y st ( B <> {} or F is having_a_unity ) & F is idempotent & F is commutative & F is associative holds 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) ) let F be BinOp of Y; ::_thesis: for B being Element of Fin X for f being Function of X,Y st ( B <> {} or F is having_a_unity ) & F is idempotent & F is commutative & F is associative holds 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) ) let B be Element of Fin X; ::_thesis: for f being Function of X,Y st ( B <> {} or F is having_a_unity ) & F is idempotent & F is commutative & F is associative holds 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) ) let f be Function of X,Y; ::_thesis: ( ( B <> {} or F is having_a_unity ) & F is idempotent & F is commutative & F is associative implies 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) ) ) assume that A1: ( B <> {} or F is having_a_unity ) and A2: F is idempotent and A3: F is commutative and A4: F is associative ; ::_thesis: 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) ) let IT be Element of Y; ::_thesis: ( 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) ) 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) ) ::_thesis: ( 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) implies IT = F \$\$ (B,f) ) proof assume IT = F \$\$ (B,f) ; ::_thesis: 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) then consider G being Function of (Fin X),Y such that A5: ( IT = G . B & ( for e being Element of Y st e is_a_unity_wrt F holds G . {} = e ) ) and A6: for x being Element of X holds G . {x} = f . x and A7: for B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B \ B9 holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) by A1, A3, A4, Def3; for B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) proof let B9 be Element of Fin X; ::_thesis: ( B9 c= B & B9 <> {} implies for x being Element of X st x in B holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) assume that A8: B9 c= B and A9: B9 <> {} ; ::_thesis: for x being Element of X st x in B holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) let x be Element of X; ::_thesis: ( x in B implies G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) assume A10: x in B ; ::_thesis: G . (B9 \/ {x}) = F . ((G . B9),(f . x)) percases ( x in B9 or not x in B9 ) ; suppose x in B9 ; ::_thesis: G . (B9 \/ {x}) = F . ((G . B9),(f . x)) then A11: B9 \/ {x} = B9 by ZFMISC_1:40; then A12: {x} c= B9 by XBOOLE_1:7; not x in B9 \ {x} by ZFMISC_1:56; then A13: x in B \ (B9 \ {x}) by A10, XBOOLE_0:def_5; percases ( B9 = {x} or B9 <> {x} ) ; supposeA14: B9 = {x} ; ::_thesis: G . (B9 \/ {x}) = F . ((G . B9),(f . x)) hence G . (B9 \/ {x}) = F . ((f . x),(f . x)) by A2, A6 .= F . ((G . B9),(f . x)) by A6, A14 ; ::_thesis: verum end; suppose B9 <> {x} ; ::_thesis: G . (B9 \/ {x}) = F . ((G . B9),(f . x)) then not B9 c= {x} by A12, XBOOLE_0:def_10; then B9 \ {x} <> {} by XBOOLE_1:37; then A15: G . ((B9 \ {.x.}) \/ {.x.}) = F . ((G . (B9 \ {.x.})),(f . x)) by A7, A8, A13, XBOOLE_1:1; thus G . (B9 \/ {x}) = F . ((G . (B9 \ {x})),(F . ((f . x),(f . x)))) by A2, A15, XBOOLE_1:39 .= F . ((F . ((G . (B9 \ {.x.})),(f . x))),(f . x)) by A4, BINOP_1:def_3 .= F . ((G . B9),(f . x)) by A11, A15, XBOOLE_1:39 ; ::_thesis: verum end; end; end; suppose not x in B9 ; ::_thesis: G . (B9 \/ {x}) = F . ((G . B9),(f . x)) then x in B \ B9 by A10, XBOOLE_0:def_5; hence G . (B9 \/ {x}) = F . ((G . B9),(f . x)) by A7, A8, A9; ::_thesis: verum end; end; end; hence 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 B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) by A5, A6; ::_thesis: verum end; given G being Function of (Fin X),Y such that A16: ( 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 ) ) and A17: for B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ; ::_thesis: IT = F \$\$ (B,f) for B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B \ B9 holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) proof let B9 be Element of Fin X; ::_thesis: ( B9 c= B & B9 <> {} implies for x being Element of X st x in B \ B9 holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) assume A18: ( B9 c= B & B9 <> {} ) ; ::_thesis: for x being Element of X st x in B \ B9 holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) let x be Element of X; ::_thesis: ( x in B \ B9 implies G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) assume x in B \ B9 ; ::_thesis: G . (B9 \/ {x}) = F . ((G . B9),(f . x)) then x in B by XBOOLE_0:def_5; hence G . (B9 \/ {x}) = F . ((G . B9),(f . x)) by A17, A18; ::_thesis: verum end; hence IT = F \$\$ (B,f) by A1, A3, A4, A16, Def3; ::_thesis: verum end; theorem Th17: :: SETWISEO:17 for Y, X being non empty set for F being BinOp of Y for f being Function of X,Y st F is commutative & F is associative holds for b being Element of X holds F \$\$ ({.b.},f) = f . b proof let Y, X be non empty set ; ::_thesis: for F being BinOp of Y for f being Function of X,Y st F is commutative & F is associative holds for b being Element of X holds F \$\$ ({.b.},f) = f . b let F be BinOp of Y; ::_thesis: for f being Function of X,Y st F is commutative & F is associative holds for b being Element of X holds F \$\$ ({.b.},f) = f . b let f be Function of X,Y; ::_thesis: ( F is commutative & F is associative implies for b being Element of X holds F \$\$ ({.b.},f) = f . b ) assume A1: ( F is commutative & F is associative ) ; ::_thesis: for b being Element of X holds F \$\$ ({.b.},f) = f . b let b be Element of X; ::_thesis: F \$\$ ({.b.},f) = f . b 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 B9 being Element of Fin X st B9 c= {b} & B9 <> {} holds for x being Element of X st x in {b} \ B9 holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) by A1, Def3; hence F \$\$ ({.b.},f) = f . b ; ::_thesis: verum end; theorem Th18: :: SETWISEO:18 for Y, X being non empty set for F being BinOp of Y for f being Function of X,Y st F is idempotent & F is commutative & F is associative holds for a, b being Element of X holds F \$\$ ({.a,b.},f) = F . ((f . a),(f . b)) proof let Y, X be non empty set ; ::_thesis: for F being BinOp of Y for f being Function of X,Y st F is idempotent & F is commutative & F is associative holds for a, b being Element of X holds F \$\$ ({.a,b.},f) = F . ((f . a),(f . b)) let F be BinOp of Y; ::_thesis: for f being Function of X,Y st F is idempotent & F is commutative & F is associative holds for a, b being Element of X holds F \$\$ ({.a,b.},f) = F . ((f . a),(f . b)) let f be Function of X,Y; ::_thesis: ( 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)) ) assume A1: ( F is idempotent & F is commutative & F is associative ) ; ::_thesis: for a, b being Element of X holds F \$\$ ({.a,b.},f) = F . ((f . a),(f . b)) let a, b be Element of X; ::_thesis: F \$\$ ({.a,b.},f) = F . ((f . a),(f . b)) 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 B9 being Element of Fin X st B9 c= {a,b} & B9 <> {} holds for x being Element of X st x in {a,b} holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) by A1, Th16; A5: b in {a,b} by TARSKI:def_2; thus F \$\$ ({.a,b.},f) = G . ({.a.} \/ {.b.}) by A2, ENUMSET1:1 .= F . ((G . {.a.}),(f . b)) by A4, A5, ZFMISC_1:7 .= F . ((f . a),(f . b)) by A3 ; ::_thesis: verum end; theorem Th19: :: SETWISEO:19 for Y, X being non empty set for F being BinOp of Y for f being Function of X,Y st F is idempotent & F is commutative & F is associative holds for a, b, c being Element of X holds F \$\$ ({.a,b,c.},f) = F . ((F . ((f . a),(f . b))),(f . c)) proof let Y, X be non empty set ; ::_thesis: for F being BinOp of Y for f being Function of X,Y st F is idempotent & F is commutative & F is associative holds for a, b, c being Element of X holds F \$\$ ({.a,b,c.},f) = F . ((F . ((f . a),(f . b))),(f . c)) let F be BinOp of Y; ::_thesis: for f being Function of X,Y st F is idempotent & F is commutative & F is associative holds for a, b, c being Element of X holds F \$\$ ({.a,b,c.},f) = F . ((F . ((f . a),(f . b))),(f . c)) let f be Function of X,Y; ::_thesis: ( 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)) ) assume A1: ( F is idempotent & F is commutative & F is associative ) ; ::_thesis: for a, b, c being Element of X holds F \$\$ ({.a,b,c.},f) = F . ((F . ((f . a),(f . b))),(f . c)) let a, b, c be Element of X; ::_thesis: F \$\$ ({.a,b,c.},f) = F . ((F . ((f . a),(f . b))),(f . c)) 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 B9 being Element of Fin X st B9 c= {a,b,c} & B9 <> {} holds for x being Element of X st x in {a,b,c} holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) by A1, Th16; A5: b in {a,b,c} by ENUMSET1:def_1; A6: G . {a,b} = G . ({a} \/ {b}) by ENUMSET1:1 .= F . ((G . {.a.}),(f . b)) by A4, A5, Th1 .= F . ((f . a),(f . b)) by A3 ; A7: c in {a,b,c} by ENUMSET1:def_1; thus F \$\$ ({.a,b,c.},f) = G . ({.a,b.} \/ {.c.}) by A2, ENUMSET1:3 .= F . ((F . ((f . a),(f . b))),(f . c)) by A4, A6, A7, Th2 ; ::_thesis: verum end; theorem Th20: :: SETWISEO:20 for Y, X 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 F is idempotent & F is commutative & F is associative & B <> {} holds for x being Element of X holds F \$\$ ((B \/ {.x.}),f) = F . ((F \$\$ (B,f)),(f . x)) proof let Y, X be non empty set ; ::_thesis: for F being BinOp of Y for B being Element of Fin X for f being Function of X,Y st F is idempotent & F is commutative & F is associative & B <> {} holds for x being Element of X holds F \$\$ ((B \/ {.x.}),f) = F . ((F \$\$ (B,f)),(f . x)) let F be BinOp of Y; ::_thesis: for B being Element of Fin X for f being Function of X,Y st F is idempotent & F is commutative & F is associative & B <> {} holds for x being Element of X holds F \$\$ ((B \/ {.x.}),f) = F . ((F \$\$ (B,f)),(f . x)) let B be Element of Fin X; ::_thesis: for f being Function of X,Y st F is idempotent & F is commutative & F is associative & B <> {} holds for x being Element of X holds F \$\$ ((B \/ {.x.}),f) = F . ((F \$\$ (B,f)),(f . x)) let f be Function of X,Y; ::_thesis: ( 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)) ) assume A1: ( F is idempotent & F is commutative & F is associative ) ; ::_thesis: ( not B <> {} or for x being Element of X holds F \$\$ ((B \/ {.x.}),f) = F . ((F \$\$ (B,f)),(f . x)) ) assume A2: B <> {} ; ::_thesis: for x being Element of X holds F \$\$ ((B \/ {.x.}),f) = F . ((F \$\$ (B,f)),(f . x)) then consider G9 being Function of (Fin X),Y such that A3: F \$\$ (B,f) = G9 . B and for e being Element of Y st e is_a_unity_wrt F holds G9 . {} = e and A4: for x being Element of X holds G9 . {x} = f . x and A5: for B9 being Element of Fin X st B9 c= B & B9 <> {} holds for x being Element of X st x in B holds G9 . (B9 \/ {x}) = F . ((G9 . B9),(f . x)) by A1, Th16; let x be Element of X; ::_thesis: F \$\$ ((B \/ {.x.}),f) = F . ((F \$\$ (B,f)),(f . x)) consider G being Function of (Fin X),Y such that A6: 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 A7: for x being Element of X holds G . {x} = f . x and A8: for B9 being Element of Fin X st B9 c= B \/ {x} & B9 <> {} holds for x9 being Element of X st x9 in B \/ {x} holds G . (B9 \/ {x9}) = F . ((G . B9),(f . x9)) by A1, Th16; defpred S1[ set ] means ( \$1 <> {} & \$1 c= B implies G . \$1 = G9 . \$1 ); A9: for B9 being Element of Fin X for b being Element of X st S1[B9] holds S1[B9 \/ {b}] proof A10: B c= B \/ {x} by XBOOLE_1:7; let C be Element of Fin X; ::_thesis: for b being Element of X st S1[C] holds S1[C \/ {b}] let y be Element of X; ::_thesis: ( S1[C] implies S1[C \/ {y}] ) assume A11: ( C <> {} & C c= B implies G . C = G9 . C ) ; ::_thesis: S1[C \/ {y}] assume that C \/ {y} <> {} and A12: C \/ {y} c= B ; ::_thesis: G . (C \/ {y}) = G9 . (C \/ {y}) A13: ( C c= B & y in B ) by A12, ZFMISC_1:137; percases ( C = {} or C <> {} ) ; supposeA14: C = {} ; ::_thesis: G . (C \/ {y}) = G9 . (C \/ {y}) hence G . (C \/ {y}) = f . y by A7 .= G9 . (C \/ {y}) by A4, A14 ; ::_thesis: verum end; supposeA15: C <> {} ; ::_thesis: G . (C \/ {y}) = G9 . (C \/ {y}) hence G . (C \/ {y}) = F . ((G9 . C),(f . y)) by A8, A11, A13, A10, XBOOLE_1:1 .= G9 . (C \/ {y}) by A5, A13, A15 ; ::_thesis: verum end; end; end; A16: S1[ {}. X] ; A17: for C being Element of Fin X holds S1[C] from SETWISEO:sch_4(A16, A9); x in B \/ {x} by ZFMISC_1:136; hence F \$\$ ((B \/ {.x.}),f) = F . ((G . B),(f . x)) by A2, A6, A8, XBOOLE_1:7 .= F . ((F \$\$ (B,f)),(f . x)) by A2, A3, A17 ; ::_thesis: verum end; theorem Th21: :: SETWISEO:21 for Y, X being non empty set for F being BinOp of Y for f being Function of X,Y st F is idempotent & F is commutative & F is associative holds for B1, B2 being Element of Fin X st B1 <> {} & B2 <> {} holds F \$\$ ((B1 \/ B2),f) = F . ((F \$\$ (B1,f)),(F \$\$ (B2,f))) proof let Y, X be non empty set ; ::_thesis: for F being BinOp of Y for f being Function of X,Y st F is idempotent & F is commutative & F is associative holds for B1, B2 being Element of Fin X st B1 <> {} & B2 <> {} holds F \$\$ ((B1 \/ B2),f) = F . ((F \$\$ (B1,f)),(F \$\$ (B2,f))) let F be BinOp of Y; ::_thesis: for f being Function of X,Y st F is idempotent & F is commutative & F is associative holds for B1, B2 being Element of Fin X st B1 <> {} & B2 <> {} holds F \$\$ ((B1 \/ B2),f) = F . ((F \$\$ (B1,f)),(F \$\$ (B2,f))) let f be Function of X,Y; ::_thesis: ( 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))) ) assume that A1: F is idempotent and A2: F is commutative and A3: F is associative ; ::_thesis: for B1, B2 being Element of Fin X st B1 <> {} & B2 <> {} holds F \$\$ ((B1 \/ B2),f) = F . ((F \$\$ (B1,f)),(F \$\$ (B2,f))) let B1, B2 be Element of Fin X; ::_thesis: ( B1 <> {} & B2 <> {} implies F \$\$ ((B1 \/ B2),f) = F . ((F \$\$ (B1,f)),(F \$\$ (B2,f))) ) defpred S1[ Element of Fin X] means ( \$1 <> {} implies F \$\$ ((B1 \/ \$1),f) = F . ((F \$\$ (B1,f)),(F \$\$ (\$1,f))) ); assume A4: B1 <> {} ; ::_thesis: ( not B2 <> {} or F \$\$ ((B1 \/ B2),f) = F . ((F \$\$ (B1,f)),(F \$\$ (B2,f))) ) A5: for B9 being Element of Fin X for b being Element of X st S1[B9] holds S1[B9 \/ {.b.}] proof let B be Element of Fin X; ::_thesis: for b being Element of X st S1[B] holds S1[B \/ {.b.}] let x be Element of X; ::_thesis: ( S1[B] implies S1[B \/ {.x.}] ) assume that A6: ( B <> {} implies F \$\$ ((B1 \/ B),f) = F . ((F \$\$ (B1,f)),(F \$\$ (B,f))) ) and B \/ {x} <> {} ; ::_thesis: F \$\$ ((B1 \/ (B \/ {.x.})),f) = F . ((F \$\$ (B1,f)),(F \$\$ ((B \/ {.x.}),f))) percases ( B = {} or B <> {} ) ; supposeA7: B = {} ; ::_thesis: F \$\$ ((B1 \/ (B \/ {.x.})),f) = F . ((F \$\$ (B1,f)),(F \$\$ ((B \/ {.x.}),f))) hence F \$\$ ((B1 \/ (B \/ {.x.})),f) = F . ((F \$\$ (B1,f)),(f . x)) by A1, A2, A3, A4, Th20 .= F . ((F \$\$ (B1,f)),(F \$\$ ((B \/ {.x.}),f))) by A2, A3, A7, Th17 ; ::_thesis: verum end; supposeA8: B <> {} ; ::_thesis: F \$\$ ((B1 \/ (B \/ {.x.})),f) = F . ((F \$\$ (B1,f)),(F \$\$ ((B \/ {.x.}),f))) 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, A2, A3, A6, A8, Th20 .= F . ((F \$\$ (B1,f)),(F . ((F \$\$ (B,f)),(f . x)))) by A3, BINOP_1:def_3 .= F . ((F \$\$ (B1,f)),(F \$\$ ((B \/ {.x.}),f))) by A1, A2, A3, A8, Th20 ; ::_thesis: verum end; end; end; A9: S1[ {}. X] ; for B2 being Element of Fin X holds S1[B2] from SETWISEO:sch_4(A9, A5); hence ( not B2 <> {} or F \$\$ ((B1 \/ B2),f) = F . ((F \$\$ (B1,f)),(F \$\$ (B2,f))) ) ; ::_thesis: verum end; theorem :: SETWISEO:22 for Y, X 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 F is commutative & F is associative & F is idempotent holds for x being Element of X st x in B holds F . ((f . x),(F \$\$ (B,f))) = F \$\$ (B,f) proof let Y, X be non empty set ; ::_thesis: for F being BinOp of Y for B being Element of Fin X for f being Function of X,Y st F is commutative & F is associative & F is idempotent holds for x being Element of X st x in B holds F . ((f . x),(F \$\$ (B,f))) = F \$\$ (B,f) let F be BinOp of Y; ::_thesis: for B being Element of Fin X for f being Function of X,Y st F is commutative & F is associative & F is idempotent holds for x being Element of X st x in B holds F . ((f . x),(F \$\$ (B,f))) = F \$\$ (B,f) let B be Element of Fin X; ::_thesis: for f being Function of X,Y st F is commutative & F is associative & F is idempotent holds for x being Element of X st x in B holds F . ((f . x),(F \$\$ (B,f))) = F \$\$ (B,f) let f be Function of X,Y; ::_thesis: ( 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) ) assume that A1: ( F is commutative & F is associative ) and A2: F is idempotent ; ::_thesis: for x being Element of X st x in B holds F . ((f . x),(F \$\$ (B,f))) = F \$\$ (B,f) let x be Element of X; ::_thesis: ( x in B implies F . ((f . x),(F \$\$ (B,f))) = F \$\$ (B,f) ) assume A3: x in B ; ::_thesis: F . ((f . x),(F \$\$ (B,f))) = F \$\$ (B,f) thus F . ((f . x),(F \$\$ (B,f))) = F . ((F \$\$ ({.x.},f)),(F \$\$ (B,f))) by A1, Th17 .= F \$\$ (({.x.} \/ B),f) by A1, A2, A3, Th21 .= F \$\$ (B,f) by A3, ZFMISC_1:40 ; ::_thesis: verum end; theorem :: SETWISEO:23 for Y, X being non empty set for F being BinOp of Y for f being Function of X,Y st F is commutative & F is associative & F is idempotent holds 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 let Y, X be non empty set ; ::_thesis: for F being BinOp of Y for f being Function of X,Y st F is commutative & F is associative & F is idempotent holds for B, C being Element of Fin X st B <> {} & B c= C holds F . ((F \$\$ (B,f)),(F \$\$ (C,f))) = F \$\$ (C,f) let F be BinOp of Y; ::_thesis: for f being Function of X,Y st F is commutative & F is associative & F is idempotent holds for B, C being Element of Fin X st B <> {} & B c= C holds F . ((F \$\$ (B,f)),(F \$\$ (C,f))) = F \$\$ (C,f) let f be Function of X,Y; ::_thesis: ( 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) ) assume A1: ( F is commutative & F is associative & F is idempotent ) ; ::_thesis: for B, C being Element of Fin X st B <> {} & B c= C holds F . ((F \$\$ (B,f)),(F \$\$ (C,f))) = F \$\$ (C,f) let B, C be Element of Fin X; ::_thesis: ( B <> {} & B c= C implies F . ((F \$\$ (B,f)),(F \$\$ (C,f))) = F \$\$ (C,f) ) assume that A2: B <> {} and A3: B c= C ; ::_thesis: F . ((F \$\$ (B,f)),(F \$\$ (C,f))) = F \$\$ (C,f) C <> {} by A2, A3; hence F . ((F \$\$ (B,f)),(F \$\$ (C,f))) = F \$\$ ((B \/ C),f) by A1, A2, Th21 .= F \$\$ (C,f) by A3, XBOOLE_1:12 ; ::_thesis: verum end; theorem Th24: :: SETWISEO:24 for Y, X 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 <> {} & F is commutative & F is associative & F is idempotent holds 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 let Y, X be non empty set ; ::_thesis: for F being BinOp of Y for B being Element of Fin X for f being Function of X,Y st B <> {} & F is commutative & F is associative & F is idempotent holds 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 let F be BinOp of Y; ::_thesis: for B being Element of Fin X for f being Function of X,Y st B <> {} & F is commutative & F is associative & F is idempotent holds 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 let B be Element of Fin X; ::_thesis: for f being Function of X,Y st B <> {} & F is commutative & F is associative & F is idempotent holds 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 let f be Function of X,Y; ::_thesis: ( 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 ) assume that A1: B <> {} and A2: ( F is commutative & F is associative ) and A3: F is idempotent ; ::_thesis: 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 let a be Element of Y; ::_thesis: ( ( for b being Element of X st b in B holds f . b = a ) implies F \$\$ (B,f) = a ) defpred S1[ Element of Fin X] means ( ( for b being Element of X st b in \$1 holds f . b = a ) implies F \$\$ (\$1,f) = a ); A4: for B1, B2 being non empty Element of Fin X st S1[B1] & S1[B2] holds S1[B1 \/ B2] proof let B1, B2 be non empty Element of Fin X; ::_thesis: ( S1[B1] & S1[B2] implies S1[B1 \/ B2] ) assume that A5: ( ( ( for b being Element of X st b in B1 holds f . b = a ) implies F \$\$ (B1,f) = a ) & ( ( for b being Element of X st b in B2 holds f . b = a ) implies F \$\$ (B2,f) = a ) ) and A6: for b being Element of X st b in B1 \/ B2 holds f . b = a ; ::_thesis: F \$\$ ((B1 \/ B2),f) = a A7: now__::_thesis:_for_b_being_Element_of_X_st_b_in_B2_holds_ f_._b_=_a let b be Element of X; ::_thesis: ( b in B2 implies f . b = a ) assume b in B2 ; ::_thesis: f . b = a then b in B1 \/ B2 by XBOOLE_0:def_3; hence f . b = a by A6; ::_thesis: verum end; now__::_thesis:_for_b_being_Element_of_X_st_b_in_B1_holds_ f_._b_=_a let b be Element of X; ::_thesis: ( b in B1 implies f . b = a ) assume b in B1 ; ::_thesis: f . b = a then b in B1 \/ B2 by XBOOLE_0:def_3; hence f . b = a by A6; ::_thesis: verum end; hence F \$\$ ((B1 \/ B2),f) = F . (a,a) by A2, A3, A5, A7, Th21 .= a by A3 ; ::_thesis: verum end; A8: for x being Element of X holds S1[{.x.}] proof let x be Element of X; ::_thesis: S1[{.x.}] assume A9: for b being Element of X st b in {x} holds f . b = a ; ::_thesis: F \$\$ ({.x.},f) = a A10: x in {x} by TARSKI:def_1; thus F \$\$ ({.x.},f) = f . x by A2, Th17 .= a by A9, A10 ; ::_thesis: verum end; for B being non empty Element of Fin X holds S1[B] from SETWISEO:sch_3(A8, A4); hence ( ( for b being Element of X st b in B holds f . b = a ) implies F \$\$ (B,f) = a ) by A1; ::_thesis: verum end; theorem Th25: :: SETWISEO:25 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 F is commutative & F is associative & F is idempotent holds for a being Element of Y st f .: B = {a} holds F \$\$ (B,f) = a proof let X, Y be non empty set ; ::_thesis: for F being BinOp of Y for B being Element of Fin X for f being Function of X,Y st F is commutative & F is associative & F is idempotent holds for a being Element of Y st f .: B = {a} holds F \$\$ (B,f) = a let F be BinOp of Y; ::_thesis: for B being Element of Fin X for f being Function of X,Y st F is commutative & F is associative & F is idempotent holds for a being Element of Y st f .: B = {a} holds F \$\$ (B,f) = a let B be Element of Fin X; ::_thesis: for f being Function of X,Y st F is commutative & F is associative & F is idempotent holds for a being Element of Y st f .: B = {a} holds F \$\$ (B,f) = a let f be Function of X,Y; ::_thesis: ( 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 ) assume A1: ( F is commutative & F is associative & F is idempotent ) ; ::_thesis: for a being Element of Y st f .: B = {a} holds F \$\$ (B,f) = a let a be Element of Y; ::_thesis: ( f .: B = {a} implies F \$\$ (B,f) = a ) assume A2: f .: B = {a} ; ::_thesis: F \$\$ (B,f) = a A3: for b being Element of X st b in B holds f . b = a proof let b be Element of X; ::_thesis: ( b in B implies f . b = a ) assume b in B ; ::_thesis: f . b = a then f . b in {a} by A2, FUNCT_2:35; hence f . b = a by TARSKI:def_1; ::_thesis: verum end; B <> {} by A2; hence F \$\$ (B,f) = a by A1, A3, Th24; ::_thesis: verum end; theorem Th26: :: SETWISEO:26 for X, Y being non empty set for F being BinOp of Y st F is commutative & F is associative & F is idempotent holds 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 let X, Y be non empty set ; ::_thesis: for F being BinOp of Y st F is commutative & F is associative & F is idempotent holds 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) let F be BinOp of Y; ::_thesis: ( 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) ) assume that A1: F is commutative and A2: F is associative and A3: F is idempotent ; ::_thesis: 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) let f, g be Function of X,Y; ::_thesis: for A, B being Element of Fin X st A <> {} & f .: A = g .: B holds F \$\$ (A,f) = F \$\$ (B,g) defpred S1[ 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: for B9 being Element of Fin X for b being Element of X st S1[B9] holds S1[B9 \/ {.b.}] proof let A be Element of Fin X; ::_thesis: for b being Element of X st S1[A] holds S1[A \/ {.b.}] let x be Element of X; ::_thesis: ( S1[A] implies S1[A \/ {.x.}] ) assume A5: ( A <> {} implies for B being Element of Fin X st f .: A = g .: B holds F \$\$ (A,f) = F \$\$ (B,g) ) ; ::_thesis: S1[A \/ {.x.}] assume A \/ {x} <> {} ; ::_thesis: for B being Element of Fin X st f .: (A \/ {.x.}) = g .: B holds F \$\$ ((A \/ {.x.}),f) = F \$\$ (B,g) let B be Element of Fin X; ::_thesis: ( f .: (A \/ {.x.}) = g .: B implies F \$\$ ((A \/ {.x.}),f) = F \$\$ (B,g) ) assume A6: f .: (A \/ {x}) = g .: B ; ::_thesis: F \$\$ ((A \/ {.x.}),f) = F \$\$ (B,g) percases ( f . x in f .: A or not f . x in f .: A ) ; suppose f . x in f .: A ; ::_thesis: F \$\$ ((A \/ {.x.}),f) = F \$\$ (B,g) then consider x9 being Element of X such that A7: x9 in A and A8: f . x9 = f . x by FUNCT_2:65; A9: g .: B = (f .: A) \/ (Im (f,x)) by A6, RELAT_1:120 .= (f .: A) \/ {(f . x)} by Th8 .= f .: A by A7, A8, FUNCT_2:35, ZFMISC_1:40 ; thus F \$\$ ((A \/ {.x.}),f) = F . ((F \$\$ (A,f)),(f . x)) by A1, A2, A3, A7, Th20 .= F . ((F \$\$ ((A \/ {.x9.}),f)),(f . x)) by A7, ZFMISC_1:40 .= F . ((F . ((F \$\$ (A,f)),(f . x9))),(f . x)) by A1, A2, A3, A7, Th20 .= F . ((F \$\$ (A,f)),(F . ((f . x9),(f . x9)))) by A2, A8, BINOP_1:def_3 .= F \$\$ ((A \/ {.x9.}),f) by A1, A2, A3, A7, Th20 .= F \$\$ (A,f) by A7, ZFMISC_1:40 .= F \$\$ (B,g) by A5, A7, A9 ; ::_thesis: verum end; supposeA10: not f . x in f .: A ; ::_thesis: F \$\$ ((A \/ {.x.}),f) = F \$\$ (B,g) percases ( A = {} or A <> {} ) ; supposeA11: A = {} ; ::_thesis: F \$\$ ((A \/ {.x.}),f) = F \$\$ (B,g) then A12: g .: B = Im (f,x) by A6 .= {(f . x)} by Th8 ; thus F \$\$ ((A \/ {.x.}),f) = f . x by A1, A2, A11, Th17 .= F \$\$ (B,g) by A1, A2, A3, A12, Th25 ; ::_thesis: verum end; supposeA13: A <> {} ; ::_thesis: F \$\$ ((A \/ {.x.}),f) = F \$\$ (B,g) reconsider B1 = B \ (g " {(f . x)}) as Element of Fin X by Th11; A14: now__::_thesis:_not_B1_=_{} assume B1 = {} ; ::_thesis: contradiction then A15: g .: B c= g .: (g " {(f . x)}) by RELAT_1:123, XBOOLE_1:37; g .: (g " {(f . x)}) c= {(f . x)} by FUNCT_1:75; then f .: (A \/ {x}) c= {(f . x)} by A6, A15, XBOOLE_1:1; then (f .: A) \/ (f .: {x}) c= {(f . x)} by RELAT_1:120; then f .: A = (f .: A) /\ {(f . x)} by XBOOLE_1:11, XBOOLE_1:28 .= {} by A10, ZFMISC_1:50, XBOOLE_0:def_7 ; hence contradiction by A13, Th13; ::_thesis: verum end; reconsider B2 = B /\ (g " {(f . x)}) as Element of Fin X by Th11, XBOOLE_1:17; A17: B = B1 \/ B2 by XBOOLE_1:51; A18: for b being Element of X st b in B2 holds g . b = f . x proof let b be Element of X; ::_thesis: ( b in B2 implies g . b = f . x ) assume b in B2 ; ::_thesis: g . b = f . x then b in g " {(f . x)} by XBOOLE_0:def_4; then g . b in {(f . x)} by FUNCT_1:def_7; hence g . b = f . x by TARSKI:def_1; ::_thesis: verum end; A19: f .: A = (f .: A) \ {(f . x)} by A10, ZFMISC_1:57 .= (f .: A) \ (Im (f,x)) by Th8 .= ((f .: A) \/ (f .: {x})) \ (f .: {x}) by XBOOLE_1:40 .= (f .: (A \/ {x})) \ (Im (f,x)) by RELAT_1:120 .= (g .: B) \ {(f . x)} by A6, Th8 .= g .: B1 by Th6 ; x in A \/ {x} by ZFMISC_1:136; then consider x9 being Element of X such that A20: x9 in B and A21: g . x9 = f . x by A6, FUNCT_2:35, FUNCT_2:65; x9 in g " {(f . x)} by A21, Th7; then A22: B2 <> {} by A20, XBOOLE_0:def_4; thus F \$\$ ((A \/ {.x.}),f) = F . ((F \$\$ (A,f)),(f . x)) by A1, A2, A3, A13, Th20 .= F . ((F \$\$ (B1,g)),(f . x)) by A5, A13, A19 .= F . ((F \$\$ (B1,g)),(F \$\$ (B2,g))) by A1, A2, A3, A22, A18, Th24 .= F \$\$ (B,g) by A1, A2, A3, A17, A14, A22, Th21 ; ::_thesis: verum end; end; end; end; end; A23: S1[ {}. X] ; A24: for A being Element of Fin X holds S1[A] from SETWISEO:sch_4(A23, A4); let A, B be Element of Fin X; ::_thesis: ( A <> {} & f .: A = g .: B implies F \$\$ (A,f) = F \$\$ (B,g) ) assume ( A <> {} & f .: A = g .: B ) ; ::_thesis: F \$\$ (A,f) = F \$\$ (B,g) hence F \$\$ (A,f) = F \$\$ (B,g) by A24; ::_thesis: verum end; theorem :: SETWISEO:27 for Y, X being non empty set for F, G being BinOp of Y st F is idempotent & F is commutative & F is associative & G is_distributive_wrt F holds for B being Element of Fin X st B <> {} holds 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 Y, X be non empty set ; ::_thesis: for F, G being BinOp of Y st F is idempotent & F is commutative & F is associative & G is_distributive_wrt F holds for B being Element of Fin X st B <> {} holds for f being Function of X,Y for a being Element of Y holds G . (a,(F \$\$ (B,f))) = F \$\$ (B,(G [;] (a,f))) let F, G be BinOp of Y; ::_thesis: ( F is idempotent & F is commutative & F is associative & G is_distributive_wrt F implies for B being Element of Fin X st B <> {} holds for f being Function of X,Y for a being Element of Y holds G . (a,(F \$\$ (B,f))) = F \$\$ (B,(G [;] (a,f))) ) assume that A1: F is idempotent and A2: ( F is commutative & F is associative ) and A3: G is_distributive_wrt F ; ::_thesis: for B being Element of Fin X st B <> {} holds for f being Function of X,Y for a being Element of Y holds G . (a,(F \$\$ (B,f))) = F \$\$ (B,(G [;] (a,f))) let B be Element of Fin X; ::_thesis: ( B <> {} implies for f being Function of X,Y for a being Element of Y holds G . (a,(F \$\$ (B,f))) = F \$\$ (B,(G [;] (a,f))) ) assume A4: B <> {} ; ::_thesis: for f being Function of X,Y for a being Element of Y holds G . (a,(F \$\$ (B,f))) = F \$\$ (B,(G [;] (a,f))) let f be Function of X,Y; ::_thesis: for a being Element of Y holds G . (a,(F \$\$ (B,f))) = F \$\$ (B,(G [;] (a,f))) let a be Element of Y; ::_thesis: G . (a,(F \$\$ (B,f))) = F \$\$ (B,(G [;] (a,f))) defpred S1[ Element of Fin X] means G . (a,(F \$\$ (\$1,f))) = F \$\$ (\$1,(G [;] (a,f))); A5: for B1, B2 being non empty Element of Fin X st S1[B1] & S1[B2] holds S1[B1 \/ B2] proof let B1, B2 be non empty Element of Fin X; ::_thesis: ( S1[B1] & S1[B2] implies S1[B1 \/ B2] ) assume A6: ( G . (a,(F \$\$ (B1,f))) = F \$\$ (B1,(G [;] (a,f))) & G . (a,(F \$\$ (B2,f))) = F \$\$ (B2,(G [;] (a,f))) ) ; ::_thesis: S1[B1 \/ B2] thus G . (a,(F \$\$ ((B1 \/ B2),f))) = G . (a,(F . ((F \$\$ (B1,f)),(F \$\$ (B2,f))))) by A1, A2, Th21 .= F . ((F \$\$ (B1,(G [;] (a,f)))),(F \$\$ (B2,(G [;] (a,f))))) by A3, A6, BINOP_1:11 .= F \$\$ ((B1 \/ B2),(G [;] (a,f))) by A1, A2, Th21 ; ::_thesis: verum end; A7: for x being Element of X holds S1[{.x.}] proof let x be Element of X; ::_thesis: S1[{.x.}] thus G . (a,(F \$\$ ({.x.},f))) = G . (a,(f . x)) by A2, Th17 .= (G [;] (a,f)) . x by FUNCOP_1:53 .= F \$\$ ({.x.},(G [;] (a,f))) by A2, Th17 ; ::_thesis: verum end; for B being non empty Element of Fin X holds S1[B] from SETWISEO:sch_3(A7, A5); hence G . (a,(F \$\$ (B,f))) = F \$\$ (B,(G [;] (a,f))) by A4; ::_thesis: verum end; theorem :: SETWISEO:28 for Y, X being non empty set for F, G being BinOp of Y st F is idempotent & F is commutative & F is associative & G is_distributive_wrt F holds for B being Element of Fin X st B <> {} holds 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 Y, X be non empty set ; ::_thesis: for F, G being BinOp of Y st F is idempotent & F is commutative & F is associative & G is_distributive_wrt F holds for B being Element of Fin X st B <> {} holds for f being Function of X,Y for a being Element of Y holds G . ((F \$\$ (B,f)),a) = F \$\$ (B,(G [:] (f,a))) let F, G be BinOp of Y; ::_thesis: ( F is idempotent & F is commutative & F is associative & G is_distributive_wrt F implies for B being Element of Fin X st B <> {} holds for f being Function of X,Y for a being Element of Y holds G . ((F \$\$ (B,f)),a) = F \$\$ (B,(G [:] (f,a))) ) assume that A1: F is idempotent and A2: ( F is commutative & F is associative ) and A3: G is_distributive_wrt F ; ::_thesis: for B being Element of Fin X st B <> {} holds for f being Function of X,Y for a being Element of Y holds G . ((F \$\$ (B,f)),a) = F \$\$ (B,(G [:] (f,a))) let B be Element of Fin X; ::_thesis: ( B <> {} implies for f being Function of X,Y for a being Element of Y holds G . ((F \$\$ (B,f)),a) = F \$\$ (B,(G [:] (f,a))) ) assume A4: B <> {} ; ::_thesis: for f being Function of X,Y for a being Element of Y holds G . ((F \$\$ (B,f)),a) = F \$\$ (B,(G [:] (f,a))) let f be Function of X,Y; ::_thesis: for a being Element of Y holds G . ((F \$\$ (B,f)),a) = F \$\$ (B,(G [:] (f,a))) let a be Element of Y; ::_thesis: G . ((F \$\$ (B,f)),a) = F \$\$ (B,(G [:] (f,a))) defpred S1[ Element of Fin X] means G . ((F \$\$ (\$1,f)),a) = F \$\$ (\$1,(G [:] (f,a))); A5: for B1, B2 being non empty Element of Fin X st S1[B1] & S1[B2] holds S1[B1 \/ B2] proof let B1, B2 be non empty Element of Fin X; ::_thesis: ( S1[B1] & S1[B2] implies S1[B1 \/ B2] ) assume A6: ( G . ((F \$\$ (B1,f)),a) = F \$\$ (B1,(G [:] (f,a))) & G . ((F \$\$ (B2,f)),a) = F \$\$ (B2,(G [:] (f,a))) ) ; ::_thesis: S1[B1 \/ B2] thus G . ((F \$\$ ((B1 \/ B2),f)),a) = G . ((F . ((F \$\$ (B1,f)),(F \$\$ (B2,f)))),a) by A1, A2, Th21 .= F . ((F \$\$ (B1,(G [:] (f,a)))),(F \$\$ (B2,(G [:] (f,a))))) by A3, A6, BINOP_1:11 .= F \$\$ ((B1 \/ B2),(G [:] (f,a))) by A1, A2, Th21 ; ::_thesis: verum end; A7: for x being Element of X holds S1[{.x.}] proof let x be Element of X; ::_thesis: S1[{.x.}] thus G . ((F \$\$ ({.x.},f)),a) = G . ((f . x),a) by A2, Th17 .= (G [:] (f,a)) . x by FUNCOP_1:48 .= F \$\$ ({.x.},(G [:] (f,a))) by A2, Th17 ; ::_thesis: verum end; for B being non empty Element of Fin X holds S1[B] from SETWISEO:sch_3(A7, A5); hence G . ((F \$\$ (B,f)),a) = F \$\$ (B,(G [:] (f,a))) by A4; ::_thesis: verum end; definition let X, Y be non empty set ; let f be Function of X,Y; let A be Element of Fin X; :: original: .: redefine funcf .: A -> Element of Fin Y; coherence f .: A is Element of Fin Y by Lm1; end; theorem Th29: :: SETWISEO:29 for A, X, Y being non empty set for F being BinOp of A st F is idempotent & F is commutative & F is associative holds for B being Element of Fin X st B <> {} holds for f being Function of X,Y 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 ; ::_thesis: for F being BinOp of A st F is idempotent & F is commutative & F is associative holds for B being Element of Fin X st B <> {} holds for f being Function of X,Y for g being Function of Y,A holds F \$\$ ((f .: B),g) = F \$\$ (B,(g * f)) let F be BinOp of A; ::_thesis: ( F is idempotent & F is commutative & F is associative implies for B being Element of Fin X st B <> {} holds for f being Function of X,Y for g being Function of Y,A holds F \$\$ ((f .: B),g) = F \$\$ (B,(g * f)) ) assume that A1: F is idempotent and A2: ( F is commutative & F is associative ) ; ::_thesis: for B being Element of Fin X st B <> {} holds for f being Function of X,Y for g being Function of Y,A holds F \$\$ ((f .: B),g) = F \$\$ (B,(g * f)) let B be Element of Fin X; ::_thesis: ( B <> {} implies for f being Function of X,Y for g being Function of Y,A holds F \$\$ ((f .: B),g) = F \$\$ (B,(g * f)) ) assume A3: B <> {} ; ::_thesis: for f being Function of X,Y for g being Function of Y,A holds F \$\$ ((f .: B),g) = F \$\$ (B,(g * f)) let f be Function of X,Y; ::_thesis: for g being Function of Y,A holds F \$\$ ((f .: B),g) = F \$\$ (B,(g * f)) let g be Function of Y,A; ::_thesis: F \$\$ ((f .: B),g) = F \$\$ (B,(g * f)) defpred S1[ Element of Fin X] means F \$\$ ((f .: \$1),g) = F \$\$ (\$1,(g * f)); A4: dom f = X by FUNCT_2:def_1; A5: for B1, B2 being non empty Element of Fin X st S1[B1] & S1[B2] holds S1[B1 \/ B2] proof let B1, B2 be non empty Element of Fin X; ::_thesis: ( S1[B1] & S1[B2] implies S1[B1 \/ B2] ) assume A6: ( F \$\$ ((f .: B1),g) = F \$\$ (B1,(g * f)) & F \$\$ ((f .: B2),g) = F \$\$ (B2,(g * f)) ) ; ::_thesis: S1[B1 \/ B2] B7: B1 c= X by FINSUB_1:def_5; B8: B2 c= X by FINSUB_1:def_5; thus F \$\$ ((f .: (B1 \/ B2)),g) = F \$\$ (((f .: B1) \/ (f .: B2)),g) by RELAT_1:120 .= F . ((F \$\$ ((f .: B1),g)),(F \$\$ ((f .: B2),g))) by A1, A2, B7, B8, Th21, A4 .= F \$\$ ((B1 \/ B2),(g * f)) by A1, A2, A6, Th21 ; ::_thesis: verum end; A9: for x being Element of X holds S1[{.x.}] proof let x be Element of X; ::_thesis: S1[{.x.}] f .: {.x.} = Im (f,x) ; hence F \$\$ ((f .: {.x.}),g) = F \$\$ ({.(f . x).},g) by A4, FUNCT_1:59 .= g . (f . x) by A2, Th17 .= (g * f) . x by FUNCT_2:15 .= F \$\$ ({.x.},(g * f)) by A2, Th17 ; ::_thesis: verum end; for B being non empty Element of Fin X holds S1[B] from SETWISEO:sch_3(A9, A5); hence F \$\$ ((f .: B),g) = F \$\$ (B,(g * f)) by A3; ::_thesis: verum end; theorem Th30: :: SETWISEO:30 for X, Y being non empty set for F being BinOp of Y st F is commutative & F is associative & F is idempotent holds for Z being non empty set for G being BinOp of Z st G is commutative & G is associative & G is idempotent holds 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)) ) holds for B being Element of Fin X st B <> {} holds g . (F \$\$ (B,f)) = G \$\$ (B,(g * f)) proof let X, Y be non empty set ; ::_thesis: for F being BinOp of Y st F is commutative & F is associative & F is idempotent holds for Z being non empty set for G being BinOp of Z st G is commutative & G is associative & G is idempotent holds 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)) ) holds for B being Element of Fin X st B <> {} holds g . (F \$\$ (B,f)) = G \$\$ (B,(g * f)) let F be BinOp of Y; ::_thesis: ( 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 holds 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)) ) holds for B being Element of Fin X st B <> {} holds g . (F \$\$ (B,f)) = G \$\$ (B,(g * f)) ) assume that A1: ( F is commutative & F is associative ) and A2: F is idempotent ; ::_thesis: for Z being non empty set for G being BinOp of Z st G is commutative & G is associative & G is idempotent holds 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)) ) holds for B being Element of Fin X st B <> {} holds g . (F \$\$ (B,f)) = G \$\$ (B,(g * f)) let Z be non empty set ; ::_thesis: for G being BinOp of Z st G is commutative & G is associative & G is idempotent holds 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)) ) holds for B being Element of Fin X st B <> {} holds g . (F \$\$ (B,f)) = G \$\$ (B,(g * f)) let G be BinOp of Z; ::_thesis: ( G is commutative & G is associative & G is idempotent implies 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)) ) holds for B being Element of Fin X st B <> {} holds g . (F \$\$ (B,f)) = G \$\$ (B,(g * f)) ) assume that A3: ( G is commutative & G is associative ) and A4: G is idempotent ; ::_thesis: 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)) ) holds for B being Element of Fin X st B <> {} holds g . (F \$\$ (B,f)) = G \$\$ (B,(g * f)) let f be Function of X,Y; ::_thesis: 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)) ) holds for B being Element of Fin X st B <> {} holds g . (F \$\$ (B,f)) = G \$\$ (B,(g * f)) let g be Function of Y,Z; ::_thesis: ( ( for x, y being Element of Y holds g . (F . (x,y)) = G . ((g . x),(g . y)) ) implies for B being Element of Fin X st B <> {} holds g . (F \$\$ (B,f)) = G \$\$ (B,(g * f)) ) assume A5: for x, y being Element of Y holds g . (F . (x,y)) = G . ((g . x),(g . y)) ; ::_thesis: for B being Element of Fin X st B <> {} holds g . (F \$\$ (B,f)) = G \$\$ (B,(g * f)) defpred S1[ Element of Fin X] means ( \$1 <> {} implies g . (F \$\$ (\$1,f)) = G \$\$ (\$1,(g * f)) ); A6: for B9 being Element of Fin X for b being Element of X st S1[B9] holds S1[B9 \/ {.b.}] proof let B be Element of Fin X; ::_thesis: for b being Element of X st S1[B] holds S1[B \/ {.b.}] let x be Element of X; ::_thesis: ( S1[B] implies S1[B \/ {.x.}] ) assume that A7: ( B <> {} implies g . (F \$\$ (B,f)) = G \$\$ (B,(g * f)) ) and B \/ {x} <> {} ; ::_thesis: g . (F \$\$ ((B \/ {.x.}),f)) = G \$\$ ((B \/ {.x.}),(g * f)) percases ( B = {} or B <> {} ) ; supposeA8: B = {} ; ::_thesis: g . (F \$\$ ((B \/ {.x.}),f)) = G \$\$ ((B \/ {.x.}),(g * f)) hence g . (F \$\$ ((B \/ {.x.}),f)) = g . (f . x) by A1, Th17 .= (g * f) . x by FUNCT_2:15 .= G \$\$ ((B \/ {.x.}),(g * f)) by A3, A8, Th17 ; ::_thesis: verum end; supposeA9: B <> {} ; ::_thesis: g . (F \$\$ ((B \/ {.x.}),f)) = G \$\$ ((B \/ {.x.}),(g * f)) hence g . (F \$\$ ((B \/ {.x.}),f)) = g . (F . ((F \$\$ (B,f)),(f . x))) by A1, A2, Th20 .= G . ((g . (F \$\$ (B,f))),(g . (f . x))) by A5 .= G . ((G \$\$ (B,(g * f))),((g * f) . x)) by A7, A9, FUNCT_2:15 .= G \$\$ ((B \/ {.x.}),(g * f)) by A3, A4, A9, Th20 ; ::_thesis: verum end; end; end; A10: S1[ {}. X] ; thus for B being Element of Fin X holds S1[B] from SETWISEO:sch_4(A10, A6); ::_thesis: verum end; theorem Th31: :: SETWISEO:31 for Y, X being non empty set for F being BinOp of Y st F is commutative & F is associative & F is having_a_unity holds for f being Function of X,Y holds F \$\$ (({}. X),f) = the_unity_wrt F proof let Y, X be non empty set ; ::_thesis: for F being BinOp of Y st F is commutative & F is associative & F is having_a_unity holds for f being Function of X,Y holds F \$\$ (({}. X),f) = the_unity_wrt F let F be BinOp of Y; ::_thesis: ( F is commutative & F is associative & F is having_a_unity implies for f being Function of X,Y holds F \$\$ (({}. X),f) = the_unity_wrt F ) assume A1: ( F is commutative & F is associative & F is having_a_unity ) ; ::_thesis: for f being Function of X,Y holds F \$\$ (({}. X),f) = the_unity_wrt F let f be Function of X,Y; ::_thesis: F \$\$ (({}. X),f) = the_unity_wrt F ( the_unity_wrt F is_a_unity_wrt F & 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 B9 being Element of Fin X st B9 c= {}. X & B9 <> {} holds for x being Element of X st x in ({}. X) \ B9 holds G . (B9 \/ {x}) = F . ((G . B9),(f . x)) ) ) ) by A1, Def3, Th14; hence F \$\$ (({}. X),f) = the_unity_wrt F ; ::_thesis: verum end; theorem Th32: :: SETWISEO:32 for Y, X 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 F is idempotent & F is commutative & F is associative & F is having_a_unity holds for x being Element of X holds F \$\$ ((B \/ {.x.}),f) = F . ((F \$\$ (B,f)),(f . x)) proof let Y, X be non empty set ; ::_thesis: for F being BinOp of Y for B being Element of Fin X for f being Function of X,Y st F is idempotent & F is commutative & F is associative & F is having_a_unity holds for x being Element of X holds F \$\$ ((B \/ {.x.}),f) = F . ((F \$\$ (B,f)),(f . x)) let F be BinOp of Y; ::_thesis: for B being Element of Fin X for f being Function of X,Y st F is idempotent & F is commutative & F is associative & F is having_a_unity holds for x being Element of X holds F \$\$ ((B \/ {.x.}),f) = F . ((F \$\$ (B,f)),(f . x)) let B be Element of Fin X; ::_thesis: for f being Function of X,Y st F is idempotent & F is commutative & F is associative & F is having_a_unity holds for x being Element of X holds F \$\$ ((B \/ {.x.}),f) = F . ((F \$\$ (B,f)),(f . x)) let f be Function of X,Y; ::_thesis: ( F is idempotent & F is commutative & F is associative & F is having_a_unity implies for x being Element of X holds F \$\$ ((B \/ {.x.}),f) = F . ((F \$\$ (B,f)),(f . x)) ) assume that A1: F is idempotent and A2: ( F is commutative & F is associative ) ; ::_thesis: ( not F is having_a_unity or for x being Element of X holds F \$\$ ((B \/ {.x.}),f) = F . ((F \$\$ (B,f)),(f . x)) ) assume A3: F is having_a_unity ; ::_thesis: for x being Element of X holds F \$\$ ((B \/ {.x.}),f) = F . ((F \$\$ (B,f)),(f . x)) let x be Element of X; ::_thesis: F \$\$ ((B \/ {.x.}),f) = F . ((F \$\$ (B,f)),(f . x)) A4: {} = {}. X ; now__::_thesis:_(_B_=_{}_implies_F_\$\$_((B_\/_{.x.}),f)_=_F_._((F_\$\$_(B,f)),(f_._x))_) assume A5: B = {} ; ::_thesis: F \$\$ ((B \/ {.x.}),f) = F . ((F \$\$ (B,f)),(f . x)) hence F \$\$ ((B \/ {.x.}),f) = f . x by A2, Th17 .= F . ((the_unity_wrt F),(f . x)) by A3, Th15 .= F . ((F \$\$ (B,f)),(f . x)) by A2, A3, A4, A5, Th31 ; ::_thesis: verum end; hence F \$\$ ((B \/ {.x.}),f) = F . ((F \$\$ (B,f)),(f . x)) by A1, A2, Th20; ::_thesis: verum end; theorem :: SETWISEO:33 for Y, X being non empty set for F being BinOp of Y for f being Function of X,Y st F is idempotent & F is commutative & F is associative & F is having_a_unity holds for B1, B2 being Element of Fin X holds F \$\$ ((B1 \/ B2),f) = F . ((F \$\$ (B1,f)),(F \$\$ (B2,f))) proof let Y, X be non empty set ; ::_thesis: for F being BinOp of Y for f being Function of X,Y st F is idempotent & F is commutative & F is associative & F is having_a_unity holds for B1, B2 being Element of Fin X holds F \$\$ ((B1 \/ B2),f) = F . ((F \$\$ (B1,f)),(F \$\$ (B2,f))) let F be BinOp of Y; ::_thesis: for f being Function of X,Y st F is idempotent & F is commutative & F is associative & F is having_a_unity holds for B1, B2 being Element of Fin X holds F \$\$ ((B1 \/ B2),f) = F . ((F \$\$ (B1,f)),(F \$\$ (B2,f))) let f be Function of X,Y; ::_thesis: ( F is idempotent & F is commutative & F is associative & F is having_a_unity implies for B1, B2 being Element of Fin X holds F \$\$ ((B1 \/ B2),f) = F . ((F \$\$ (B1,f)),(F \$\$ (B2,f))) ) assume that A1: F is idempotent and A2: ( F is commutative & F is associative ) and A3: F is having_a_unity ; ::_thesis: for B1, B2 being Element of Fin X holds F \$\$ ((B1 \/ B2),f) = F . ((F \$\$ (B1,f)),(F \$\$ (B2,f))) let B1, B2 be Element of Fin X; ::_thesis: F \$\$ ((B1 \/ B2),f) = F . ((F \$\$ (B1,f)),(F \$\$ (B2,f))) now__::_thesis:_(_(_B1_=_{}_or_B2_=_{}_)_implies_F_\$\$_((B1_\/_B2),f)_=_F_._((F_\$\$_(B1,f)),(F_\$\$_(B2,f)))_) A4: {} = {}. X ; assume A5: ( B1 = {} or B2 = {} ) ; ::_thesis: F \$\$ ((B1 \/ B2),f) = F . ((F \$\$ (B1,f)),(F \$\$ (B2,f))) percases ( B2 = {} or B1 = {} ) by A5; supposeA6: B2 = {} ; ::_thesis: F \$\$ ((B1 \/ B2),f) = F . ((F \$\$ (B1,f)),(F \$\$ (B2,f))) hence F \$\$ ((B1 \/ B2),f) = F . ((F \$\$ (B1,f)),(the_unity_wrt F)) by A3, Th15 .= F . ((F \$\$ (B1,f)),(F \$\$ (B2,f))) by A2, A3, A4, A6, Th31 ; ::_thesis: verum end; supposeA7: B1 = {} ; ::_thesis: F \$\$ ((B1 \/ B2),f) = F . ((F \$\$ (B1,f)),(F \$\$ (B2,f))) hence F \$\$ ((B1 \/ B2),f) = F . ((the_unity_wrt F),(F \$\$ (B2,f))) by A3, Th15 .= F . ((F \$\$ (B1,f)),(F \$\$ (B2,f))) by A2, A3, A4, A7, Th31 ; ::_thesis: verum end; end; end; hence F \$\$ ((B1 \/ B2),f) = F . ((F \$\$ (B1,f)),(F \$\$ (B2,f))) by A1, A2, Th21; ::_thesis: verum end; theorem :: SETWISEO:34 for X, Y being non empty set for F being BinOp of Y st F is commutative & F is associative & F is idempotent & F is having_a_unity holds 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 let X, Y be non empty set ; ::_thesis: for F being BinOp of Y st F is commutative & F is associative & F is idempotent & F is having_a_unity holds 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) let F be BinOp of Y; ::_thesis: ( F is commutative & F is associative & F is idempotent & F is having_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) ) assume that A1: ( F is commutative & F is associative ) and A2: F is idempotent and A3: F is having_a_unity ; ::_thesis: 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) let f, g be Function of X,Y; ::_thesis: for A, B being Element of Fin X st f .: A = g .: B holds F \$\$ (A,f) = F \$\$ (B,g) let A, B be Element of Fin X; ::_thesis: ( f .: A = g .: B implies F \$\$ (A,f) = F \$\$ (B,g) ) assume A4: f .: A = g .: B ; ::_thesis: F \$\$ (A,f) = F \$\$ (B,g) now__::_thesis:_(_A_=_{}_implies_F_\$\$_(A,f)_=_F_\$\$_(B,g)_) assume A5: A = {} ; ::_thesis: F \$\$ (A,f) = F \$\$ (B,g) then A = {}. X ; then A6: F \$\$ (A,f) = the_unity_wrt F by A1, A3, Th31; f .: A = {} by A5; then B = {}. X by A4, Th13; hence F \$\$ (A,f) = F \$\$ (B,g) by A1, A3, A6, Th31; ::_thesis: verum end; hence F \$\$ (A,f) = F \$\$ (B,g) by A1, A2, A4, Th26; ::_thesis: verum end; theorem Th35: :: SETWISEO:35 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 is having_a_unity holds for B being Element of Fin X for f being Function of X,Y 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 ; ::_thesis: for F being BinOp of A st F is idempotent & F is commutative & F is associative & F is having_a_unity holds for B being Element of Fin X for f being Function of X,Y for g being Function of Y,A holds F \$\$ ((f .: B),g) = F \$\$ (B,(g * f)) let F be BinOp of A; ::_thesis: ( F is idempotent & F is commutative & F is associative & F is having_a_unity implies for B being Element of Fin X for f being Function of X,Y for g being Function of Y,A holds F \$\$ ((f .: B),g) = F \$\$ (B,(g * f)) ) assume that A1: F is idempotent and A2: ( F is commutative & F is associative ) and A3: F is having_a_unity ; ::_thesis: for B being Element of Fin X for f being Function of X,Y for g being Function of Y,A holds F \$\$ ((f .: B),g) = F \$\$ (B,(g * f)) let B be Element of Fin X; ::_thesis: for f being Function of X,Y for g being Function of Y,A holds F \$\$ ((f .: B),g) = F \$\$ (B,(g * f)) let f be Function of X,Y; ::_thesis: for g being Function of Y,A holds F \$\$ ((f .: B),g) = F \$\$ (B,(g * f)) let g be Function of Y,A; ::_thesis: F \$\$ ((f .: B),g) = F \$\$ (B,(g * f)) now__::_thesis:_(_B_=_{}_implies_F_\$\$_((f_.:_B),g)_=_F_\$\$_(B,(g_*_f))_) assume A4: B = {} ; ::_thesis: F \$\$ ((f .: B),g) = F \$\$ (B,(g * f)) then f .: B = {}. Y ; then A5: F \$\$ ((f .: B),g) = the_unity_wrt F by A2, A3, Th31; B = {}. X by A4; hence F \$\$ ((f .: B),g) = F \$\$ (B,(g * f)) by A2, A3, A5, Th31; ::_thesis: verum end; hence F \$\$ ((f .: B),g) = F \$\$ (B,(g * f)) by A1, A2, Th29; ::_thesis: verum end; theorem :: SETWISEO:36 for X, Y being non empty set for F being BinOp of Y st F is commutative & F is associative & F is idempotent & F is having_a_unity holds for Z being non empty set for G being BinOp of Z st G is commutative & G is associative & G is idempotent & G is having_a_unity holds 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)) ) holds for B being Element of Fin X holds g . (F \$\$ (B,f)) = G \$\$ (B,(g * f)) proof let X, Y be non empty set ; ::_thesis: for F being BinOp of Y st F is commutative & F is associative & F is idempotent & F is having_a_unity holds for Z being non empty set for G being BinOp of Z st G is commutative & G is associative & G is idempotent & G is having_a_unity holds 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)) ) holds for B being Element of Fin X holds g . (F \$\$ (B,f)) = G \$\$ (B,(g * f)) let F be BinOp of Y; ::_thesis: ( F is commutative & F is associative & F is idempotent & F is having_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 is having_a_unity holds 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)) ) holds for B being Element of Fin X holds g . (F \$\$ (B,f)) = G \$\$ (B,(g * f)) ) assume that A1: ( F is commutative & F is associative ) and A2: F is idempotent and A3: F is having_a_unity ; ::_thesis: for Z being non empty set for G being BinOp of Z st G is commutative & G is associative & G is idempotent & G is having_a_unity holds 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)) ) holds for B being Element of Fin X holds g . (F \$\$ (B,f)) = G \$\$ (B,(g * f)) let Z be non empty set ; ::_thesis: for G being BinOp of Z st G is commutative & G is associative & G is idempotent & G is having_a_unity holds 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)) ) holds for B being Element of Fin X holds g . (F \$\$ (B,f)) = G \$\$ (B,(g * f)) let G be BinOp of Z; ::_thesis: ( G is commutative & G is associative & G is idempotent & G is having_a_unity implies 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)) ) holds for B being Element of Fin X holds g . (F \$\$ (B,f)) = G \$\$ (B,(g * f)) ) assume that A4: ( G is commutative & G is associative ) and A5: G is idempotent and A6: G is having_a_unity ; ::_thesis: 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)) ) holds for B being Element of Fin X holds g . (F \$\$ (B,f)) = G \$\$ (B,(g * f)) let f be Function of X,Y; ::_thesis: 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)) ) holds for B being Element of Fin X holds g . (F \$\$ (B,f)) = G \$\$ (B,(g * f)) let g be Function of Y,Z; ::_thesis: ( 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)) ) implies for B being Element of Fin X holds g . (F \$\$ (B,f)) = G \$\$ (B,(g * f)) ) assume that A7: g . (the_unity_wrt F) = the_unity_wrt G and A8: for x, y being Element of Y holds g . (F . (x,y)) = G . ((g . x),(g . y)) ; ::_thesis: for B being Element of Fin X holds g . (F \$\$ (B,f)) = G \$\$ (B,(g * f)) let B be Element of Fin X; ::_thesis: g . (F \$\$ (B,f)) = G \$\$ (B,(g * f)) percases ( B = {} or B <> {} ) ; suppose B = {} ; ::_thesis: g . (F \$\$ (B,f)) = G \$\$ (B,(g * f)) then A9: B = {}. X ; hence g . (F \$\$ (B,f)) = g . (the_unity_wrt F) by A1, A3, Th31 .= G \$\$ (B,(g * f)) by A4, A6, A7, A9, Th31 ; ::_thesis: verum end; suppose B <> {} ; ::_thesis: g . (F \$\$ (B,f)) = G \$\$ (B,(g * f)) hence g . (F \$\$ (B,f)) = G \$\$ (B,(g * f)) by A1, A2, A4, A5, A8, Th30; ::_thesis: verum end; end; end; definition let A be set ; func FinUnion A -> BinOp of (Fin A) means :Def4: :: SETWISEO:def 4 for x, y being Element of Fin A holds it . (x,y) = x \/ y; existence ex b1 being BinOp of (Fin A) st for x, y being Element of Fin A holds b1 . (x,y) = x \/ y proof deffunc H1( Element of Fin A, 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) = H1(x,y) from BINOP_1:sch_4(); hence ex b1 being BinOp of (Fin A) st for x, y being Element of Fin A holds b1 . (x,y) = x \/ y ; ::_thesis: verum end; uniqueness for b1, b2 being BinOp of (Fin A) st ( for x, y being Element of Fin A holds b1 . (x,y) = x \/ y ) & ( for x, y being Element of Fin A holds b2 . (x,y) = x \/ y ) holds b1 = b2 proof let IT, IT9 be BinOp of (Fin A); ::_thesis: ( ( for x, y being Element of Fin A holds IT . (x,y) = x \/ y ) & ( for x, y being Element of Fin A holds IT9 . (x,y) = x \/ y ) implies IT = IT9 ) assume 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 IT9 . (x,y) = x \/ y ; ::_thesis: IT = IT9 now__::_thesis:_for_x,_y_being_Element_of_Fin_A_holds_IT_._(x,y)_=_IT9_._(x,y) let x, y be Element of 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 Def4 defines FinUnion SETWISEO:def_4_:_ for A being set for b2 being BinOp of (Fin A) holds ( b2 = FinUnion A iff for x, y being Element of Fin A holds b2 . (x,y) = x \/ y ); theorem Th37: :: SETWISEO:37 for A being set holds FinUnion A is idempotent proof let A be set ; ::_thesis: FinUnion A is idempotent let x be Element of Fin A; :: according to BINOP_1:def_4 ::_thesis: (FinUnion A) . (x,x) = x thus (FinUnion A) . (x,x) = x \/ x by Def4 .= x ; ::_thesis: verum end; theorem Th38: :: SETWISEO:38 for A being set holds FinUnion A is commutative proof let A be set ; ::_thesis: FinUnion A is commutative let x be Element of Fin A; :: according to BINOP_1:def_2 ::_thesis: for b1 being Element of Fin A holds (FinUnion A) . (x,b1) = (FinUnion A) . (b1,x) let y be Element of Fin A; ::_thesis: (FinUnion A) . (x,y) = (FinUnion A) . (y,x) thus (FinUnion A) . (x,y) = y \/ x by Def4 .= (FinUnion A) . (y,x) by Def4 ; ::_thesis: verum end; theorem Th39: :: SETWISEO:39 for A being set holds FinUnion A is associative proof let A be set ; ::_thesis: FinUnion A is associative let x be Element of Fin A; :: according to BINOP_1:def_3 ::_thesis: for b1, b2 being Element of Fin A holds (FinUnion A) . (x,((FinUnion A) . (b1,b2))) = (FinUnion A) . (((FinUnion A) . (x,b1)),b2) let y, z be Element of Fin A; ::_thesis: (FinUnion A) . (x,((FinUnion A) . (y,z))) = (FinUnion A) . (((FinUnion A) . (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 ; ::_thesis: verum end; theorem Th40: :: SETWISEO:40 for A being set holds {}. A is_a_unity_wrt FinUnion A proof let A be set ; ::_thesis: {}. A is_a_unity_wrt FinUnion A thus for x being Element of Fin A holds (FinUnion A) . (({}. A),x) = x :: according to BINOP_1:def_7,BINOP_1:def_16 ::_thesis: {}. A is_a_right_unity_wrt FinUnion A proof let x be Element of Fin A; ::_thesis: (FinUnion A) . (({}. A),x) = x thus (FinUnion A) . (({}. A),x) = {} \/ x by Def4 .= x ; ::_thesis: verum end; let x be Element of Fin A; :: according to BINOP_1:def_17 ::_thesis: (FinUnion A) . (x,({}. A)) = x thus (FinUnion A) . (x,({}. A)) = x \/ {} by Def4 .= x ; ::_thesis: verum end; theorem Th41: :: SETWISEO:41 for A being set holds FinUnion A is having_a_unity proof let A be set ; ::_thesis: FinUnion A is having_a_unity {}. A is_a_unity_wrt FinUnion A by Th40; hence FinUnion A is having_a_unity by Def2; ::_thesis: verum end; theorem :: SETWISEO:42 for A being set holds the_unity_wrt (FinUnion A) is_a_unity_wrt FinUnion A proof let A be set ; ::_thesis: the_unity_wrt (FinUnion A) is_a_unity_wrt FinUnion A thus the_unity_wrt (FinUnion A) is_a_unity_wrt FinUnion A by Th14, Th41; ::_thesis: verum end; theorem Th43: :: SETWISEO:43 for A being set holds the_unity_wrt (FinUnion A) = {} proof let A be set ; ::_thesis: the_unity_wrt (FinUnion A) = {} {}. A is_a_unity_wrt FinUnion A by Th40; hence the_unity_wrt (FinUnion A) = {} by BINOP_1:def_8; ::_thesis: verum end; 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); func FinUnion (B,f) -> Element of Fin A equals :: SETWISEO:def 5 (FinUnion A) \$\$ (B,f); coherence (FinUnion A) \$\$ (B,f) is Element of Fin A ; end; :: deftheorem defines FinUnion SETWISEO:def_5_:_ 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) holds FinUnion (B,f) = (FinUnion A) \$\$ (B,f); theorem :: SETWISEO:44 for X being non empty set for A being set for f being Function of X,(Fin A) for i being Element of X holds FinUnion ({.i.},f) = f . i proof let X be non empty set ; ::_thesis: for A being set for f being Function of X,(Fin A) for i being Element of X holds FinUnion ({.i.},f) = f . i let A be set ; ::_thesis: for f being Function of X,(Fin A) for i being Element of X holds FinUnion ({.i.},f) = f . i let f be Function of X,(Fin A); ::_thesis: for i being Element of X holds FinUnion ({.i.},f) = f . i let i be Element of X; ::_thesis: FinUnion ({.i.},f) = f . i FinUnion A is commutative by Th38; hence FinUnion ({.i.},f) = f . i by Th17, Th39; ::_thesis: verum end; theorem :: SETWISEO:45 for X being non empty set for A being set for f being Function of X,(Fin A) for i, j being Element of X holds FinUnion ({.i,j.},f) = (f . i) \/ (f . j) proof let X be non empty set ; ::_thesis: for A being set for f being Function of X,(Fin A) for i, j being Element of X holds FinUnion ({.i,j.},f) = (f . i) \/ (f . j) let A be set ; ::_thesis: for f being Function of X,(Fin A) for i, j being Element of X holds FinUnion ({.i,j.},f) = (f . i) \/ (f . j) let f be Function of X,(Fin A); ::_thesis: for i, j being Element of X holds FinUnion ({.i,j.},f) = (f . i) \/ (f . j) let i, j be Element of X; ::_thesis: FinUnion ({.i,j.},f) = (f . i) \/ (f . j) ( FinUnion A is idempotent & FinUnion A is commutative ) by Th37, Th38; hence FinUnion ({.i,j.},f) = (FinUnion A) . ((f . i),(f . j)) by Th18, Th39 .= (f . i) \/ (f . j) by Def4 ; ::_thesis: verum end; theorem :: SETWISEO:46 for X being non empty set for A being set for f being Function of X,(Fin A) for i, j, k being Element of X holds FinUnion ({.i,j,k.},f) = ((f . i) \/ (f . j)) \/ (f . k) proof let X be non empty set ; ::_thesis: for A being set for f being Function of X,(Fin A) for i, j, k being Element of X holds FinUnion ({.i,j,k.},f) = ((f . i) \/ (f . j)) \/ (f . k) let A be set ; ::_thesis: for f being Function of X,(Fin A) for i, j, k being Element of X holds FinUnion ({.i,j,k.},f) = ((f . i) \/ (f . j)) \/ (f . k) let f be Function of X,(Fin A); ::_thesis: for i, j, k being Element of X holds FinUnion ({.i,j,k.},f) = ((f . i) \/ (f . j)) \/ (f . k) let i, j, k be Element of X; ::_thesis: FinUnion ({.i,j,k.},f) = ((f . i) \/ (f . j)) \/ (f . k) ( FinUnion A is idempotent & FinUnion A is commutative ) by Th37, Th38; hence FinUnion ({.i,j,k.},f) = (FinUnion A) . (((FinUnion A) . ((f . i),(f . j))),(f . k)) by Th19, Th39 .= (FinUnion A) . (((f . i) \/ (f . j)),(f . k)) by Def4 .= ((f . i) \/ (f . j)) \/ (f . k) by Def4 ; ::_thesis: verum end; theorem Th47: :: SETWISEO:47 for X being non empty set for A being set for f being Function of X,(Fin A) holds FinUnion (({}. X),f) = {} proof let X be non empty set ; ::_thesis: for A being set for f being Function of X,(Fin A) holds FinUnion (({}. X),f) = {} let A be set ; ::_thesis: for f being Function of X,(Fin A) holds FinUnion (({}. X),f) = {} let f be Function of X,(Fin A); ::_thesis: FinUnion (({}. X),f) = {} ( FinUnion A is commutative & FinUnion A is associative ) by Th38, Th39; hence FinUnion (({}. X),f) = the_unity_wrt (FinUnion A) by Th31, Th41 .= {} by Th43 ; ::_thesis: verum end; theorem Th48: :: SETWISEO:48 for X being non empty set for A being set for f being Function of X,(Fin A) for i being Element of X for B being Element of Fin X holds FinUnion ((B \/ {.i.}),f) = (FinUnion (B,f)) \/ (f . i) proof let X be non empty set ; ::_thesis: for A being set for f being Function of X,(Fin A) for i being Element of X for B being Element of Fin X holds FinUnion ((B \/ {.i.}),f) = (FinUnion (B,f)) \/ (f . i) let A be set ; ::_thesis: for f being Function of X,(Fin A) for i being Element of X for B being Element of Fin X holds FinUnion ((B \/ {.i.}),f) = (FinUnion (B,f)) \/ (f . i) let f be Function of X,(Fin A); ::_thesis: for i being Element of X for B being Element of Fin X holds FinUnion ((B \/ {.i.}),f) = (FinUnion (B,f)) \/ (f . i) let i be Element of X; ::_thesis: for B being Element of Fin X holds FinUnion ((B \/ {.i.}),f) = (FinUnion (B,f)) \/ (f . i) let B be Element of Fin X; ::_thesis: FinUnion ((B \/ {.i.}),f) = (FinUnion (B,f)) \/ (f . i) A1: FinUnion A is associative by Th39; ( FinUnion A is idempotent & FinUnion A is commutative ) by Th37, Th38; hence FinUnion ((B \/ {.i.}),f) = (FinUnion A) . ((FinUnion (B,f)),(f . i)) by A1, Th32, Th41 .= (FinUnion (B,f)) \/ (f . i) by Def4 ; ::_thesis: verum end; theorem Th49: :: SETWISEO:49 for X being non empty set for A being set for f being Function of X,(Fin A) for B being Element of Fin X holds FinUnion (B,f) = union (f .: B) proof let X be non empty set ; ::_thesis: for A being set for f being Function of X,(Fin A) for B being Element of Fin X holds FinUnion (B,f) = union (f .: B) let A be set ; ::_thesis: for f being Function of X,(Fin A) for B being Element of Fin X holds FinUnion (B,f) = union (f .: B) let f be Function of X,(Fin A); ::_thesis: for B being Element of Fin X holds FinUnion (B,f) = union (f .: B) defpred S1[ Element of Fin X] means FinUnion (\$1,f) = union (f .: \$1); A1: for B being Element of Fin X for i being Element of X st S1[B] holds S1[B \/ {.i.}] proof let B be Element of Fin X; ::_thesis: for i being Element of X st S1[B] holds S1[B \/ {.i.}] let i be Element of X; ::_thesis: ( S1[B] implies S1[B \/ {.i.}] ) assume FinUnion (B,f) = union (f .: B) ; ::_thesis: S1[B \/ {.i.}] hence FinUnion ((B \/ {.i.}),f) = (union (f .: B)) \/ (f . i) by Th48 .= (union (f .: B)) \/ (union {(f . i)}) by ZFMISC_1:25 .= union ((f .: B) \/ {(f . i)}) by ZFMISC_1:78 .= union ((f .: B) \/ (Im (f,i))) by Th8 .= union (f .: (B \/ {i})) by RELAT_1:120 ; ::_thesis: verum end; FinUnion (({}. X),f) = union (f .: ({}. X)) by Th47, ZFMISC_1:2; then A2: S1[ {}. X] ; thus for B being Element of Fin X holds S1[B] from SETWISEO:sch_4(A2, A1); ::_thesis: verum end; theorem :: SETWISEO:50 for X being non empty set for A being set for f being Function of X,(Fin A) for B1, B2 being Element of Fin X holds FinUnion ((B1 \/ B2),f) = (FinUnion (B1,f)) \/ (FinUnion (B2,f)) proof let X be non empty set ; ::_thesis: for A being set for f being Function of X,(Fin A) for B1, B2 being Element of Fin X holds FinUnion ((B1 \/ B2),f) = (FinUnion (B1,f)) \/ (FinUnion (B2,f)) let A be set ; ::_thesis: for f being Function of X,(Fin A) for B1, B2 being Element of Fin X holds FinUnion ((B1 \/ B2),f) = (FinUnion (B1,f)) \/ (FinUnion (B2,f)) let f be Function of X,(Fin A); ::_thesis: for B1, B2 being Element of Fin X holds FinUnion ((B1 \/ B2),f) = (FinUnion (B1,f)) \/ (FinUnion (B2,f)) let B1, B2 be Element of Fin X; ::_thesis: FinUnion ((B1 \/ B2),f) = (FinUnion (B1,f)) \/ (FinUnion (B2,f)) thus FinUnion ((B1 \/ B2),f) = union (f .: (B1 \/ B2)) by Th49 .= union ((f .: B1) \/ (f .: B2)) by RELAT_1:120 .= (union (f .: B1)) \/ (union (f .: B2)) by ZFMISC_1:78 .= (FinUnion (B1,f)) \/ (union (f .: B2)) by Th49 .= (FinUnion (B1,f)) \/ (FinUnion (B2,f)) by Th49 ; ::_thesis: verum end; theorem :: SETWISEO:51 for X, Y being non empty set for A being set for B being Element of Fin X for f being Function of X,Y for g being Function of Y,(Fin A) holds FinUnion ((f .: B),g) = FinUnion (B,(g * f)) proof let X, Y be non empty set ; ::_thesis: for A being set for B being Element of Fin X for f being Function of X,Y for g being Function of Y,(Fin A) holds FinUnion ((f .: B),g) = FinUnion (B,(g * f)) let A be set ; ::_thesis: for B being Element of Fin X for f being Function of X,Y for g being Function of Y,(Fin A) holds FinUnion ((f .: B),g) = FinUnion (B,(g * f)) let B be Element of Fin X; ::_thesis: for f being Function of X,Y for g being Function of Y,(Fin A) holds FinUnion ((f .: B),g) = FinUnion (B,(g * f)) let f be Function of X,Y; ::_thesis: for g being Function of Y,(Fin A) holds FinUnion ((f .: B),g) = FinUnion (B,(g * f)) let g be Function of Y,(Fin A); ::_thesis: FinUnion ((f .: B),g) = FinUnion (B,(g * f)) thus FinUnion ((f .: B),g) = union (g .: (f .: B)) by Th49 .= union ((g * f) .: B) by RELAT_1:126 .= FinUnion (B,(g * f)) by Th49 ; ::_thesis: verum end; theorem Th52: :: SETWISEO:52 for A, X being non empty set for Y being set for G being BinOp of A st G is commutative & G is associative & G is idempotent holds for B being Element of Fin X st B <> {} holds for f being Function of X,(Fin Y) for 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 ; ::_thesis: for Y being set for G being BinOp of A st G is commutative & G is associative & G is idempotent holds for B being Element of Fin X st B <> {} holds for f being Function of X,(Fin Y) for 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)) let Y be set ; ::_thesis: for G being BinOp of A st G is commutative & G is associative & G is idempotent holds for B being Element of Fin X st B <> {} holds for f being Function of X,(Fin Y) for 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)) let G be BinOp of A; ::_thesis: ( G is commutative & G is associative & G is idempotent implies for B being Element of Fin X st B <> {} holds for f being Function of X,(Fin Y) for 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)) ) assume A1: ( G is commutative & G is associative & G is idempotent ) ; ::_thesis: for B being Element of Fin X st B <> {} holds for f being Function of X,(Fin Y) for 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)) let B be Element of Fin X; ::_thesis: ( B <> {} implies for f being Function of X,(Fin Y) for 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)) ) assume A2: B <> {} ; ::_thesis: for f being Function of X,(Fin Y) for 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)) let f be Function of X,(Fin Y); ::_thesis: for 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)) let g be Function of (Fin Y),A; ::_thesis: ( ( for x, y being Element of Fin Y holds g . (x \/ y) = G . ((g . x),(g . y)) ) implies g . (FinUnion (B,f)) = G \$\$ (B,(g * f)) ) assume A3: for x, y being Element of Fin Y holds g . (x \/ y) = G . ((g . x),(g . y)) ; ::_thesis: g . (FinUnion (B,f)) = G \$\$ (B,(g * f)) A4: now__::_thesis:_for_x,_y_being_Element_of_Fin_Y_holds_g_._((FinUnion_Y)_._(x,y))_=_G_._((g_._x),(g_._y)) let x, y be Element of Fin Y; ::_thesis: g . ((FinUnion Y) . (x,y)) = G . ((g . x),(g . y)) thus g . ((FinUnion Y) . (x,y)) = g . (x \/ y) by Def4 .= G . ((g . x),(g . y)) by A3 ; ::_thesis: verum end; A5: FinUnion Y is idempotent by Th37; ( FinUnion Y is commutative & FinUnion Y is associative ) by Th38, Th39; hence g . (FinUnion (B,f)) = G \$\$ (B,(g * f)) by A1, A5, A2, A4, Th30; ::_thesis: verum end; theorem Th53: :: SETWISEO:53 for X, Z being non empty set for Y being set for G being BinOp of Z st G is commutative & G is associative & G is idempotent & G is having_a_unity holds 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)) ) holds for B being Element of Fin X holds g . (FinUnion (B,f)) = G \$\$ (B,(g * f)) proof let X, Z be non empty set ; ::_thesis: for Y being set for G being BinOp of Z st G is commutative & G is associative & G is idempotent & G is having_a_unity holds 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)) ) holds for B being Element of Fin X holds g . (FinUnion (B,f)) = G \$\$ (B,(g * f)) let Y be set ; ::_thesis: for G being BinOp of Z st G is commutative & G is associative & G is idempotent & G is having_a_unity holds 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)) ) holds for B being Element of Fin X holds g . (FinUnion (B,f)) = G \$\$ (B,(g * f)) let G be BinOp of Z; ::_thesis: ( G is commutative & G is associative & G is idempotent & G is having_a_unity implies 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)) ) holds for B being Element of Fin X holds g . (FinUnion (B,f)) = G \$\$ (B,(g * f)) ) assume that A1: ( G is commutative & G is associative ) and A2: G is idempotent and A3: G is having_a_unity ; ::_thesis: 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)) ) holds for B being Element of Fin X holds g . (FinUnion (B,f)) = G \$\$ (B,(g * f)) let f be Function of X,(Fin Y); ::_thesis: 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)) ) holds for B being Element of Fin X holds g . (FinUnion (B,f)) = G \$\$ (B,(g * f)) let g be Function of (Fin Y),Z; ::_thesis: ( g . ({}. Y) = the_unity_wrt G & ( for x, y being Element of Fin Y holds g . (x \/ y) = G . ((g . x),(g . y)) ) implies for B being Element of Fin X holds g . (FinUnion (B,f)) = G \$\$ (B,(g * f)) ) assume that A4: g . ({}. Y) = the_unity_wrt G and A5: for x, y being Element of Fin Y holds g . (x \/ y) = G . ((g . x),(g . y)) ; ::_thesis: for B being Element of Fin X holds g . (FinUnion (B,f)) = G \$\$ (B,(g * f)) let B be Element of Fin X; ::_thesis: g . (FinUnion (B,f)) = G \$\$ (B,(g * f)) A6: {} = {}. X ; A7: {} = {}. (Fin Y) ; percases ( B = {} or B <> {} ) ; supposeA8: B = {} ; ::_thesis: g . (FinUnion (B,f)) = G \$\$ (B,(g * f)) then A9: f .: B = {} ; thus g . (FinUnion (B,f)) = g . ({}. Y) by A6, A8, Th47 .= G \$\$ ((f .: B),g) by A1, A3, A4, A7, A9, Th31 .= G \$\$ (B,(g * f)) by A1, A2, A3, Th35 ; ::_thesis: verum end; suppose B <> {} ; ::_thesis: g . (FinUnion (B,f)) = G \$\$ (B,(g * f)) hence g . (FinUnion (B,f)) = G \$\$ (B,(g * f)) by A1, A2, A5, Th52; ::_thesis: verum end; end; end; definition let A be set ; func singleton A -> Function of A,(Fin A) means :Def6: :: SETWISEO:def 6 for x being set st x in A holds it . x = {x}; existence ex b1 being Function of A,(Fin A) st for x being set st x in A holds b1 . x = {x} proof deffunc H1( set ) -> set = {\$1}; A1: now__::_thesis:_for_x_being_set_st_x_in_A_holds_ H1(x)_in_Fin_A let x be set ; ::_thesis: ( x in A implies H1(x) in Fin A ) assume A2: x in A ; ::_thesis: H1(x) in Fin A then reconsider A9 = A as non empty set ; reconsider x9 = x as Element of A9 by A2; {.x9.} in Fin A9 ; hence H1(x) in Fin A ; ::_thesis: verum end; thus ex f being Function of A,(Fin A) st for x being set st x in A holds f . x = H1(x) from FUNCT_2:sch_2(A1); ::_thesis: verum end; uniqueness for b1, b2 being Function of A,(Fin A) st ( for x being set st x in A holds b1 . x = {x} ) & ( for x being set st x in A holds b2 . x = {x} ) holds b1 = b2 proof let IT, IT9 be Function of A,(Fin A); ::_thesis: ( ( for x being set st x in A holds IT . x = {x} ) & ( for x being set st x in A holds IT9 . x = {x} ) implies IT = IT9 ) assume 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 IT9 . x = {x} ; ::_thesis: IT = IT9 now__::_thesis:_for_x_being_set_st_x_in_A_holds_ IT_._x_=_IT9_._x let x be set ; ::_thesis: ( x in A implies IT . x = IT9 . x ) assume A5: x in A ; ::_thesis: IT . x = IT9 . x then IT . x = {x} by A3; hence IT . x = IT9 . x by A4, A5; ::_thesis: verum end; hence IT = IT9 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def6 defines singleton SETWISEO:def_6_:_ for A being set for b2 being Function of A,(Fin A) holds ( b2 = singleton A iff for x being set st x in A holds b2 . x = {x} ); theorem Th54: :: SETWISEO:54 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 ; ::_thesis: for f being Function of A,(Fin A) holds ( f = singleton A iff for x being Element of A holds f . x = {x} ) let f be Function of A,(Fin A); ::_thesis: ( f = singleton A iff for x being Element of A holds f . x = {x} ) thus ( f = singleton A implies for x being Element of A holds f . x = {x} ) by Def6; ::_thesis: ( ( for x being Element of A holds f . x = {x} ) implies f = singleton A ) assume for x being Element of A holds f . x = {x} ; ::_thesis: f = singleton A then for x being set st x in A holds f . x = {x} ; hence f = singleton A by Def6; ::_thesis: verum end; theorem Th55: :: SETWISEO:55 for X being non empty set for x being set for y being Element of X holds ( x in (singleton X) . y iff x = y ) proof let X be non empty set ; ::_thesis: for x being set for y being Element of X holds ( x in (singleton X) . y iff x = y ) let x be set ; ::_thesis: for y being Element of X holds ( x in (singleton X) . y iff x = y ) let y be Element of X; ::_thesis: ( x in (singleton X) . y iff x = y ) (singleton X) . y = {y} by Th54; hence ( x in (singleton X) . y iff x = y ) by TARSKI:def_1; ::_thesis: verum end; theorem :: SETWISEO:56 for X being non empty set 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 be non empty set ; ::_thesis: for x, y, z being Element of X st x in (singleton X) . z & y in (singleton X) . z holds x = y let x, y, z be Element of X; ::_thesis: ( x in (singleton X) . z & y in (singleton X) . z implies x = y ) assume that A1: x in (singleton X) . z and A2: y in (singleton X) . z ; ::_thesis: x = y x = z by A1, Th55; hence x = y by A2, Th55; ::_thesis: verum end; Lm2: for D being non empty set for X, P being set for f being Function of X,D holds f .: P c= D ; theorem Th57: :: SETWISEO:57 for X being non empty set for A being set for f being Function of X,(Fin A) for B being Element of Fin X for 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 X be non empty set ; ::_thesis: for A being set for f being Function of X,(Fin A) for B being Element of Fin X for x being set holds ( x in FinUnion (B,f) iff ex i being Element of X st ( i in B & x in f . i ) ) let A be set ; ::_thesis: for f being Function of X,(Fin A) for B being Element of Fin X for x being set holds ( x in FinUnion (B,f) iff ex i being Element of X st ( i in B & x in f . i ) ) let f be Function of X,(Fin A); ::_thesis: for B being Element of Fin X for x being set holds ( x in FinUnion (B,f) iff ex i being Element of X st ( i in B & x in f . i ) ) let B be Element of Fin X; ::_thesis: for x being set holds ( x in FinUnion (B,f) iff ex i being Element of X st ( i in B & x in f . i ) ) let x be set ; ::_thesis: ( x in FinUnion (B,f) iff ex i being Element of X st ( i in B & x in f . i ) ) A1: now__::_thesis:_(_x_in_union_(f_.:_B)_implies_ex_i9_being_Element_of_X_st_ (_i9_in_B_&_x_in_f_._i9_)_) assume x in union (f .: B) ; ::_thesis: ex i9 being Element of X st ( i9 in B & x in f . i9 ) 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 = 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:65; take i9 = i; ::_thesis: ( i9 in B & x in f . i9 ) thus ( i9 in B & x in f . i9 ) by A2, A4; ::_thesis: verum end; now__::_thesis:_(_ex_i_being_Element_of_X_st_ (_i_in_B_&_x_in_f_._i_)_implies_x_in_union_(f_.:_B)_) given i being Element of X such that A5: i in B and A6: x in f . i ; ::_thesis: x in union (f .: B) f . i in f .: B by A5, FUNCT_2:35; hence x in union (f .: B) by A6, TARSKI:def_4; ::_thesis: verum end; hence ( x in FinUnion (B,f) iff ex i being Element of X st ( i in B & x in f . i ) ) by A1, Th49; ::_thesis: verum end; theorem :: SETWISEO:58 for X being non empty set for B being Element of Fin X holds FinUnion (B,(singleton X)) = B proof let X be non empty set ; ::_thesis: for B being Element of Fin X holds FinUnion (B,(singleton X)) = B let B be Element of Fin X; ::_thesis: FinUnion (B,(singleton X)) = B now__::_thesis:_for_x_being_set_holds_ (_(_x_in_FinUnion_(B,(singleton_X))_implies_x_in_B_)_&_(_x_in_B_implies_x_in_FinUnion_(B,(singleton_X))_)_) let x be set ; ::_thesis: ( ( x in FinUnion (B,(singleton X)) implies x in B ) & ( x in B implies x in FinUnion (B,(singleton X)) ) ) thus ( x in FinUnion (B,(singleton X)) implies x in B ) ::_thesis: ( x in B implies x in FinUnion (B,(singleton X)) ) proof assume x in FinUnion (B,(singleton X)) ; ::_thesis: x in B then ex i being Element of X st ( i in B & x in (singleton X) . i ) by Th57; hence x in B by Th55; ::_thesis: verum end; assume A1: x in B ; ::_thesis: x in FinUnion (B,(singleton X)) then reconsider x9 = x as Element of X by Th9; x in (singleton X) . x9 by Th55; hence x in FinUnion (B,(singleton X)) by A1, Th57; ::_thesis: verum end; hence FinUnion (B,(singleton X)) = B by TARSKI:1; ::_thesis: verum end; theorem :: SETWISEO:59 for X being non empty set 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) ) holds for B being Element of Fin X holds g . (FinUnion (B,f)) = FinUnion (B,(g * f)) proof let X be non empty set ; ::_thesis: 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) ) holds for B being Element of Fin X holds g . (FinUnion (B,f)) = FinUnion (B,(g * f)) let Y, Z be set ; ::_thesis: 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) ) holds for B being Element of Fin X holds g . (FinUnion (B,f)) = FinUnion (B,(g * f)) let f be Function of X,(Fin Y); ::_thesis: 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) ) holds for B being Element of Fin X holds g . (FinUnion (B,f)) = FinUnion (B,(g * f)) let g be Function of (Fin Y),(Fin Z); ::_thesis: ( g . ({}. Y) = {}. Z & ( for x, y being Element of Fin Y holds g . (x \/ y) = (g . x) \/ (g . y) ) implies for B being Element of Fin X holds g . (FinUnion (B,f)) = FinUnion (B,(g * f)) ) assume that A1: g . ({}. Y) = {}. Z and A2: for x, y being Element of Fin Y holds g . (x \/ y) = (g . x) \/ (g . y) ; ::_thesis: for B being Element of Fin X holds g . (FinUnion (B,f)) = FinUnion (B,(g * f)) A3: g . ({}. Y) = the_unity_wrt (FinUnion Z) by A1, Th43; A4: now__::_thesis:_for_x,_y_being_Element_of_Fin_Y_holds_g_._(x_\/_y)_=_(FinUnion_Z)_._((g_._x),(g_._y)) let x, y be Element of Fin Y; ::_thesis: g . (x \/ y) = (FinUnion Z) . ((g . x),(g . y)) thus g . (x \/ y) = (g . x) \/ (g . y) by A2 .= (FinUnion Z) . ((g . x),(g . y)) by Def4 ; ::_thesis: verum end; let B be Element of Fin X; ::_thesis: g . (FinUnion (B,f)) = FinUnion (B,(g * f)) A5: FinUnion Z is idempotent by Th37; ( FinUnion Z is associative & FinUnion Z is commutative ) by Th38, Th39; hence g . (FinUnion (B,f)) = FinUnion (B,(g * f)) by A5, A3, A4, Th41, Th53; ::_thesis: verum end;