let A be non empty finite set ; :: thesis: for U being Function of (bool A),(bool A) st U . {} = {} & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) holds
ex R being non empty finite RelStr st
( the carrier of R = A & U = UAp R )
let L be Function of (bool A),(bool A); :: thesis: ( L . {} = {} & ( for X, Y being Subset of A holds L . (X \/ Y) = (L . X) \/ (L . Y) ) implies ex R being non empty finite RelStr st
( the carrier of R = A & L = UAp R ) )
assume that
A1: L . {} = {} and
A2: for X, Y being Subset of A holds L . (X \/ Y) = (L . X) \/ (L . Y) ; :: thesis: ex R being non empty finite RelStr st
( the carrier of R = A & L = UAp R )
defpred S₁[ set , set ] means $1 in L . {$2};
consider R being Relation of A such that
A3: for x, y being Element of A holds
( [x,y] in R iff S₁[x,y] ) from RELSET_1:sch 2();
reconsider RR = RelStr(# A,R #) as non empty finite RelStr ;
take RR ; :: thesis: ( the carrier of RR = A & L = UAp RR )
A4: for y being Element of RR
for Y being Subset of RR st Y = {y} holds
UAp Y = L . Y

proof

let y be Element of RR; :: thesis: for Y being Subset of RR st Y = {y} holds
UAp Y = L . Y
let Y be Subset of RR; :: thesis: ( Y = {y} implies UAp Y = L . Y )
assume A5: Y = {y} ; :: thesis: UAp Y = L . Y
thus UAp Y c= L . Y :: according to XBOOLE_0:def 10 :: thesis: L . Y c= UAp Y

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in UAp Y or x in L . Y )
assume x in UAp Y ; :: thesis: x in L . Y
then consider a being Element of RR such that
A6: ( a = x & Class ( the InternalRel of RR,a) meets Y ) ;
consider z being object such that
A7: ( z in Class ( the InternalRel of RR,a) & z in Y ) by A6, XBOOLE_0:3;
z = y by A7, TARSKI:def 1, A5;
then [x,y] in R by A6, A7, EQREL_1:18;
hence x in L . Y by A5, A3, A6; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in L . Y or x in UAp Y )
assume A8: x in L . Y ; :: thesis: x in UAp Y
A9: y in Y by TARSKI:def 1, A5;
A10: L . Y in bool A by FUNCT_2:5;
then [x,y] in R by A3, A8, A5;
then y in Class (R,x) by EQREL_1:18;
then Class ( the InternalRel of RR,x) meets Y by A9, XBOOLE_0:3;
hence x in UAp Y by A10, A8; :: thesis: verum

end;

dom L = bool A by FUNCT_2:def 1;
then A11: dom (UAp RR) = dom L by FUNCT_2:def 1;
for x being object st x in dom (UAp RR) holds
(UAp RR) . x = L . x

proof

let x be object ; :: thesis: ( x in dom (UAp RR) implies (UAp RR) . x = L . x )
assume A12: x in dom (UAp RR) ; :: thesis: (UAp RR) . x = L . x

per cases ( x <> {} or x = {} ) ;

suppose x <> {} ; :: thesis: (UAp RR) . x = L . x

then reconsider X = x as non empty finite Subset of RR by A12;
defpred S₂[ non empty finite Subset of RR] means (UAp RR) . $1 = L . $1;
A13: for x being Element of RR st x in X holds
S₂[{x}]

proof

let x be Element of RR; :: thesis: ( x in X implies S₂[{x}] )
assume x in X ; :: thesis: S₂[{x}]
set I = {x};
(UAp RR) . {x} = UAp {x} by Def11
.= L . {x} by A4 ;
hence S₂[{x}] ; :: thesis: verum

end;

A14: for x being Element of RR
for B being non empty finite Subset of RR st x in X & B c= X & not x in B & S₂[B] holds
S₂[B \/ {x}]

proof

let x be Element of RR; :: thesis: for B being non empty finite Subset of RR st x in X & B c= X & not x in B & S₂[B] holds
S₂[B \/ {x}]
let B be non empty finite Subset of RR; :: thesis: ( x in X & B c= X & not x in B & S₂[B] implies S₂[B \/ {x}] )
assume ( x in X & B c= X & not x in B & S₂[B] ) ; :: thesis: S₂[B \/ {x}]
then A15: UAp B = L . B by Def11;
set I = {x};
(UAp RR) . (B \/ {x}) = UAp (B \/ {x}) by Def11
.= (UAp B) \/ (UAp {x}) by Th13
.= (L . B) \/ (L . {x}) by A4, A15
.= L . (B \/ {x}) by A2 ;
hence S₂[B \/ {x}] ; :: thesis: verum

end;

S₂[X] from CHAIN_1:sch 2(A13, A14);
hence (UAp RR) . x = L . x ; :: thesis: verum

end;

suppose A16: x = {} ; :: thesis: (UAp RR) . x = L . x

UAp ({} RR) = L . {} by A1;
hence (UAp RR) . x = L . x by Def11, A16; :: thesis: verum

end;

end;

end;

hence ( the carrier of RR = A & L = UAp RR ) by A11, FUNCT_1:2; :: thesis: verum