let X be non empty set ; :: thesis: ex f being Function of (BoolePoset X),(product (X --> (BoolePoset 1))) st
( f is isomorphic & ( for Y being Subset of X holds f . Y = chi (Y,X) ) )
set XB = X --> (BoolePoset 1);
deffunc H₁( set ) -> Element of bool [:X,{{},1}:] = chi ($1,X);
consider f being Function such that
A1: dom f = bool X and
A2: for Y being set st Y in bool X holds
f . Y = H₁(Y) from FUNCT_1:sch 3();
LattPOSet (BooleLatt 1) = RelStr(# the carrier of (BooleLatt 1),(LattRel (BooleLatt 1)) #) by LATTICE3:def 2;
then A3: the carrier of (BoolePoset 1) = the carrier of (BooleLatt 1) by YELLOW_1:def 2
.= bool {{}} by CARD_1:49, LATTICE3:def 1
.= {0,1} by CARD_1:49, ZFMISC_1:24 ;
A4: rng f c= product (Carrier (X --> (BoolePoset 1)))

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in product (Carrier (X --> (BoolePoset 1))) )
assume y in rng f ; :: thesis: y in product (Carrier (X --> (BoolePoset 1)))
then consider x being set such that
A5: ( x in dom f & y = f . x ) by FUNCT_1:def 3;
A6: dom (chi (x,X)) = X by FUNCT_3:def 3
.= dom (Carrier (X --> (BoolePoset 1))) by PARTFUN1:def 2 ;
A7: for z being set st z in dom (Carrier (X --> (BoolePoset 1))) holds
(chi (x,X)) . z in (Carrier (X --> (BoolePoset 1))) . z

proof

let z be set ; :: thesis: ( z in dom (Carrier (X --> (BoolePoset 1))) implies (chi (x,X)) . z in (Carrier (X --> (BoolePoset 1))) . z )
assume z in dom (Carrier (X --> (BoolePoset 1))) ; :: thesis: (chi (x,X)) . z in (Carrier (X --> (BoolePoset 1))) . z
then A8: z in X by PARTFUN1:def 2;
then ex R being 1-sorted st
( R = (X --> (BoolePoset 1)) . z & (Carrier (X --> (BoolePoset 1))) . z = the carrier of R ) by PRALG_1:def 13;
then A9: (Carrier (X --> (BoolePoset 1))) . z = {0,1} by A3, A8, FUNCOP_1:7;

per cases ( z in x or not z in x ) ;

suppose z in x ; :: thesis: (chi (x,X)) . z in (Carrier (X --> (BoolePoset 1))) . z

then (chi (x,X)) . z = 1 by A8, FUNCT_3:def 3;
hence (chi (x,X)) . z in (Carrier (X --> (BoolePoset 1))) . z by A9, TARSKI:def 2; :: thesis: verum

end;

suppose not z in x ; :: thesis: (chi (x,X)) . z in (Carrier (X --> (BoolePoset 1))) . z

then (chi (x,X)) . z = 0 by A8, FUNCT_3:def 3;
hence (chi (x,X)) . z in (Carrier (X --> (BoolePoset 1))) . z by A9, TARSKI:def 2; :: thesis: verum

end;

end;

end;

chi (x,X) = y by A1, A2, A5;
hence y in product (Carrier (X --> (BoolePoset 1))) by A6, A7, CARD_3:def 5; :: thesis: verum

end;

LattPOSet (BooleLatt X) = RelStr(# the carrier of (BooleLatt X),(LattRel (BooleLatt X)) #) by LATTICE3:def 2;
then A10: the carrier of (BoolePoset X) = the carrier of (BooleLatt X) by YELLOW_1:def 2
.= bool X by LATTICE3:def 1 ;
A11: the carrier of (product (X --> (BoolePoset 1))) = product (Carrier (X --> (BoolePoset 1))) by YELLOW_1:def 4;
then reconsider f = f as Function of (BoolePoset X),(product (X --> (BoolePoset 1))) by A10, A1, A4, FUNCT_2:def 1, RELSET_1:4;
A12: for A, B being Element of (BoolePoset X) holds
( A <= B iff f . A <= f . B )

proof

let A, B be Element of (BoolePoset X); :: thesis: ( A <= B iff f . A <= f . B )
A13: ( f . A = chi (A,X) & f . B = chi (B,X) ) by A10, A2;

hereby :: thesis: ( f . A <= f . B implies A <= B )

assume A <= B ; :: thesis: f . A <= f . B
then A14: A c= B by YELLOW_1:2;
for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> (BoolePoset 1)) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )

proof

let i be set ; :: thesis: ( i in X implies ex R being RelStr ex xi, yi being Element of R st
( R = (X --> (BoolePoset 1)) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi ) )
assume A15: i in X ; :: thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (X --> (BoolePoset 1)) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
take R = BoolePoset 1; :: thesis: ex xi, yi being Element of R st
( R = (X --> (BoolePoset 1)) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )

per cases ( i in A or not i in A ) ;

suppose A16: i in A ; :: thesis: ex xi, yi being Element of R st
( R = (X --> (BoolePoset 1)) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )

reconsider xi = 1, yi = 1 as Element of R by A3, TARSKI:def 2;
take xi ; :: thesis: ex yi being Element of R st
( R = (X --> (BoolePoset 1)) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
take yi ; :: thesis: ( R = (X --> (BoolePoset 1)) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
thus R = (X --> (BoolePoset 1)) . i by A15, FUNCOP_1:7; :: thesis: ( xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
thus xi = (chi (A,X)) . i by A15, A16, FUNCT_3:def 3; :: thesis: ( yi = (chi (B,X)) . i & xi <= yi )
thus yi = (chi (B,X)) . i by A14, A15, A16, FUNCT_3:def 3; :: thesis: xi <= yi
thus xi <= yi ; :: thesis: verum

end;

suppose A17: not i in A ; :: thesis: ex xi, yi being Element of R st
( R = (X --> (BoolePoset 1)) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )

thus ex xi, yi being Element of R st
( R = (X --> (BoolePoset 1)) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi ) :: thesis: verum

proof

per cases ( i in B or not i in B ) ;

suppose A18: i in B ; :: thesis: ex xi, yi being Element of R st
( R = (X --> (BoolePoset 1)) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )

reconsider xi = 0 , yi = 1 as Element of R by A3, TARSKI:def 2;
take xi ; :: thesis: ex yi being Element of R st
( R = (X --> (BoolePoset 1)) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
take yi ; :: thesis: ( R = (X --> (BoolePoset 1)) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
thus R = (X --> (BoolePoset 1)) . i by A15, FUNCOP_1:7; :: thesis: ( xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
thus xi = (chi (A,X)) . i by A15, A17, FUNCT_3:def 3; :: thesis: ( yi = (chi (B,X)) . i & xi <= yi )
thus yi = (chi (B,X)) . i by A15, A18, FUNCT_3:def 3; :: thesis: xi <= yi
xi c= yi by XBOOLE_1:2;
hence xi <= yi by YELLOW_1:2; :: thesis: verum

end;

suppose A19: not i in B ; :: thesis: ex xi, yi being Element of R st
( R = (X --> (BoolePoset 1)) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )

reconsider xi = 0 , yi = 0 as Element of R by A3, TARSKI:def 2;
take xi ; :: thesis: ex yi being Element of R st
( R = (X --> (BoolePoset 1)) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
take yi ; :: thesis: ( R = (X --> (BoolePoset 1)) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
thus R = (X --> (BoolePoset 1)) . i by A15, FUNCOP_1:7; :: thesis: ( xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
thus xi = (chi (A,X)) . i by A15, A17, FUNCT_3:def 3; :: thesis: ( yi = (chi (B,X)) . i & xi <= yi )
thus yi = (chi (B,X)) . i by A15, A19, FUNCT_3:def 3; :: thesis: xi <= yi
thus xi <= yi ; :: thesis: verum

end;

end;

end;

end;

end;

end;

hence f . A <= f . B by A11, A13, YELLOW_1:def 4; :: thesis: verum

end;

assume f . A <= f . B ; :: thesis: A <= B
then consider h1, h2 being Function such that
A20: h1 = f . A and
A21: h2 = f . B and
A22: for i being set st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> (BoolePoset 1)) . i & xi = h1 . i & yi = h2 . i & xi <= yi ) by A11, YELLOW_1:def 4;
A c= B

proof

let i be set ; :: according to TARSKI:def 3 :: thesis: ( not i in A or i in B )
assume A23: i in A ; :: thesis: i in B
then consider R being RelStr , xi, yi being Element of R such that
A24: R = (X --> (BoolePoset 1)) . i and
A25: xi = h1 . i and
A26: yi = h2 . i and
A27: xi <= yi by A10, A22;
reconsider a = xi, b = yi as Element of (BoolePoset 1) by A10, A23, A24, FUNCOP_1:7;
A28: a <= b by A10, A23, A24, A27, FUNCOP_1:7;
A29: xi = (chi (A,X)) . i by A10, A2, A20, A25
.= 1 by A10, A23, FUNCT_3:def 3 ;
A30: yi <> 0

proof

assume yi = 0 ; :: thesis: contradiction
then 1 c= 0 by A29, A28, YELLOW_1:2;
hence contradiction ; :: thesis: verum

end;

A31: R = BoolePoset 1 by A10, A23, A24, FUNCOP_1:7;
(chi (B,X)) . i = h2 . i by A10, A2, A21
.= 1 by A3, A26, A31, A30, TARSKI:def 2 ;
hence i in B by FUNCT_3:36; :: thesis: verum

end;

hence A <= B by YELLOW_1:2; :: thesis: verum

end;

product (Carrier (X --> (BoolePoset 1))) c= rng f

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in product (Carrier (X --> (BoolePoset 1))) or z in rng f )
assume z in product (Carrier (X --> (BoolePoset 1))) ; :: thesis: z in rng f
then consider g being Function such that
A32: z = g and
A33: dom g = dom (Carrier (X --> (BoolePoset 1))) and
A34: for y being set st y in dom (Carrier (X --> (BoolePoset 1))) holds
g . y in (Carrier (X --> (BoolePoset 1))) . y by CARD_3:def 5;
set A = g " {1};
A35: g " {1} c= X

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in g " {1} or a in X )
assume a in g " {1} ; :: thesis: a in X
then a in dom g by FUNCT_1:def 7;
hence a in X by A33, PARTFUN1:def 2; :: thesis: verum

end;

A36: dom (chi ((g " {1}),X)) = X by FUNCT_3:def 3
.= dom g by A33, PARTFUN1:def 2 ;
for a being set st a in dom (chi ((g " {1}),X)) holds
(chi ((g " {1}),X)) . a = g . a

proof

let a be set ; :: thesis: ( a in dom (chi ((g " {1}),X)) implies (chi ((g " {1}),X)) . a = g . a )
assume A37: a in dom (chi ((g " {1}),X)) ; :: thesis: (chi ((g " {1}),X)) . a = g . a
then a in X ;
then a in dom (Carrier (X --> (BoolePoset 1))) by PARTFUN1:def 2;
then A38: g . a in (Carrier (X --> (BoolePoset 1))) . a by A34;
ex R being 1-sorted st
( R = (X --> (BoolePoset 1)) . a & (Carrier (X --> (BoolePoset 1))) . a = the carrier of R ) by A37, PRALG_1:def 13;
then (Carrier (X --> (BoolePoset 1))) . a = {0,1} by A3, A37, FUNCOP_1:7;
then A39: ( g . a = 0 or g . a = 1 ) by A38, TARSKI:def 2;

per cases ( a in g " {1} or not a in g " {1} ) ;

suppose a in g " {1} ; :: thesis: (chi ((g " {1}),X)) . a = g . a

then ( (chi ((g " {1}),X)) . a = 1 & g . a in {1} ) by A37, FUNCT_1:def 7, FUNCT_3:def 3;
hence (chi ((g " {1}),X)) . a = g . a by TARSKI:def 1; :: thesis: verum

end;

suppose A40: not a in g " {1} ; :: thesis: (chi ((g " {1}),X)) . a = g . a

g . a <> 1

proof

assume g . a = 1 ; :: thesis: contradiction
then g . a in {1} by TARSKI:def 1;
hence contradiction by A36, A37, A40, FUNCT_1:def 7; :: thesis: verum

end;

hence (chi ((g " {1}),X)) . a = g . a by A37, A39, A40, FUNCT_3:def 3; :: thesis: verum

end;

end;

end;

then z = chi ((g " {1}),X) by A32, A36, FUNCT_1:2
.= f . (g " {1}) by A2, A35 ;
hence z in rng f by A1, A35, FUNCT_1:def 3; :: thesis: verum

end;

then A41: rng f = the carrier of (product (X --> (BoolePoset 1))) by A11, XBOOLE_0:def 10;
take f ; :: thesis: ( f is isomorphic & ( for Y being Subset of X holds f . Y = chi (Y,X) ) )
for A, B being Element of (BoolePoset X) st f . A = f . B holds
A = B

proof

let A, B be Element of (BoolePoset X); :: thesis: ( f . A = f . B implies A = B )
assume A42: f . A = f . B ; :: thesis: A = B
( f . A = chi (A,X) & f . B = chi (B,X) ) by A10, A2;
hence A = B by A10, A42, FUNCT_3:38; :: thesis: verum

end;

then f is one-to-one by WAYBEL_1:def 1;
hence f is isomorphic by A41, A12, WAYBEL_0:66; :: thesis: for Y being Subset of X holds f . Y = chi (Y,X)
thus for Y being Subset of X holds f . Y = chi (Y,X) by A2; :: thesis: verum