let X be non empty set ; :: thesis: ex f being Function of (BoolePoset X),(product (X --> (BoolePoset {0}))) st
( f is isomorphic & ( for Y being Subset of X holds f . Y = chi (Y,X) ) )
set XB = X --> (BoolePoset {0});
deffunc H₁( set ) -> Element of K19(K20(X,{0,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 5();
LattPOSet (BooleLatt {0}) = RelStr(# the carrier of (BooleLatt {0}),(LattRel (BooleLatt {0})) #) by LATTICE3:def 2;
then A3: the carrier of (BoolePoset {0}) = the carrier of (BooleLatt {0}) by YELLOW_1:def 2
.= bool {{}} by LATTICE3:def 1
.= {0,1} by CARD_1:49, ZFMISC_1:24 ;
A4: rng f c= product (Carrier (X --> (BoolePoset {0})))

proof

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

proof

let z be object ; :: thesis: ( z in dom (Carrier (X --> (BoolePoset {0}))) implies (chi (x,X)) . z in (Carrier (X --> (BoolePoset {0}))) . z )
assume z in dom (Carrier (X --> (BoolePoset {0}))) ; :: thesis: (chi (x,X)) . z in (Carrier (X --> (BoolePoset {0}))) . z
then A8: z in X ;
then ex R being 1-sorted st
( R = (X --> (BoolePoset {0})) . z & (Carrier (X --> (BoolePoset {0}))) . z = the carrier of R ) by PRALG_1:def 15;
then A9: (Carrier (X --> (BoolePoset {0}))) . 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 {0}))) . z

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

end;

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

then (chi (x,X)) . z = 0 by A8, FUNCT_3:def 3;
hence (chi (x,X)) . z in (Carrier (X --> (BoolePoset {0}))) . 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 {0}))) 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 {0}))) = product (Carrier (X --> (BoolePoset {0}))) by YELLOW_1:def 4;
then reconsider f = f as Function of (BoolePoset X),(product (X --> (BoolePoset {0}))) 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 object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> (BoolePoset {0})) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )

proof

let i be object ; :: thesis: ( i in X implies ex R being RelStr ex xi, yi being Element of R st
( R = (X --> (BoolePoset {0})) . 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 {0})) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
take R = BoolePoset {0}; :: thesis: ex xi, yi being Element of R st
( R = (X --> (BoolePoset {0})) . 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 {0})) . 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 {0})) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
take yi ; :: thesis: ( R = (X --> (BoolePoset {0})) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
thus R = (X --> (BoolePoset {0})) . 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 {0})) . 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 {0})) . 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 {0})) . 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 {0})) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
take yi ; :: thesis: ( R = (X --> (BoolePoset {0})) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
thus R = (X --> (BoolePoset {0})) . 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 ;
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 {0})) . 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 {0})) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
take yi ; :: thesis: ( R = (X --> (BoolePoset {0})) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
thus R = (X --> (BoolePoset {0})) . 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 object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> (BoolePoset {0})) . i & xi = h1 . i & yi = h2 . i & xi <= yi ) by A11, YELLOW_1:def 4;
A c= B

proof

let i be object ; :: 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 {0})) . 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 {0}) 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 {0} c= 0 by A29, A28, YELLOW_1:2, CARD_1:49;
hence contradiction ; :: thesis: verum

end;

A31: R = BoolePoset {0} 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 {0}))) c= rng f

proof

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

proof

let a be object ; :: 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; :: 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 object st a in dom (chi ((g " {1}),X)) holds
(chi ((g " {1}),X)) . a = g . a

proof

let a be object ; :: 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 {0}))) by PARTFUN1:def 2;
then A38: g . a in (Carrier (X --> (BoolePoset {0}))) . a by A34;
ex R being 1-sorted st
( R = (X --> (BoolePoset {0})) . a & (Carrier (X --> (BoolePoset {0}))) . a = the carrier of R ) by A37, PRALG_1:def 15;
then (Carrier (X --> (BoolePoset {0}))) . 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 {0}))) by A11;
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 ;
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