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 S1[ 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 S1[x,y] ) from 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 ;
z = y by ;
then [x,y] in R by ;
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 ;
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 ;
hence x in UAp Y by ; :: 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 S2[ non empty finite Subset of RR] means (UAp RR) . \$1 = L . \$1;
A13: for x being Element of RR st x in X holds
S2[{x}]
proof
let x be Element of RR; :: thesis: ( x in X implies S2[{x}] )
assume x in X ; :: thesis: S2[{x}]
set I = {x};
(UAp RR) . {x} = UAp {x} by Def11
.= L . {x} by A4 ;
hence S2[{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 & S2[B] holds
S2[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 & S2[B] holds
S2[B \/ {x}]

let B be non empty finite Subset of RR; :: thesis: ( x in X & B c= X & not x in B & S2[B] implies S2[B \/ {x}] )
assume ( x in X & B c= X & not x in B & S2[B] ) ; :: thesis: S2[B \/ {x}]
then A15: UAp B = L . B by Def11;
set I = {x};
(UAp RR) . (B \/ {x}) = UAp (B \/ {x}) by Def11
.= (UAp B) \/ () by Th13
.= (L . B) \/ (L . {x}) by
.= L . (B \/ {x}) by A2 ;
hence S2[B \/ {x}] ; :: thesis: verum
end;
S2[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 ; :: thesis: verum
end;
end;
end;
hence ( the carrier of RR = A & L = UAp RR ) by ; :: thesis: verum