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