let Z be set ; :: thesis: ex f being Function of (BoolePoset Z),((BoolePoset 1) |^ Z) st
( f is isomorphic & ( for Y being Subset of Z holds f . Y = chi Y,Z ) )

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

suppose A1: Z = {} ; :: thesis: ex f being Function of (BoolePoset Z),((BoolePoset 1) |^ Z) st
( f is isomorphic & ( for Y being Subset of Z holds f . Y = chi Y,Z ) )

then A2: ( BoolePoset Z = InclPoset (bool {} ) & InclPoset (bool {} ) = RelStr(# (bool {} ),(RelIncl (bool {} )) #) & (BoolePoset 1) |^ Z = RelStr(# {{} },(id {{} }) #) ) by YELLOW_1:4, YELLOW_1:27, YELLOW_1:def 1;
A3: ( dom (id {{} }) = {{} } & rng (id {{} }) = {{} } ) by RELAT_1:71;
reconsider f = id {{} } as Function of (BoolePoset Z),((BoolePoset 1) |^ Z) by A2, ZFMISC_1:1;
take f ; :: thesis: ( f is isomorphic & ( for Y being Subset of Z holds f . Y = chi Y,Z ) )
for x, y being Element of (BoolePoset Z) holds
( x <= y iff f . x <= f . y ) by A2;
hence f is isomorphic by A2, A3, WAYBEL_0:66; :: thesis: for Y being Subset of Z holds f . Y = chi Y,Z
let Y be Subset of Z; :: thesis: f . Y = chi Y,Z
Y = {} by A1;
then Y in {{} } by TARSKI:def 1;
then ( f . Y = {} & dom (chi Y,Z) = {} ) by A1, FUNCT_1:35;
hence f . Y = chi Y,Z ; :: thesis: verum

end;

suppose Z <> {} ; :: thesis: ex f being Function of (BoolePoset Z),((BoolePoset 1) |^ Z) st
( f is isomorphic & ( for Y being Subset of Z holds f . Y = chi Y,Z ) )

then reconsider Z' = Z as non empty set ;
(BoolePoset 1) |^ Z = product (Z' --> (BoolePoset 1)) by YELLOW_1:def 5;
hence ex f being Function of (BoolePoset Z),((BoolePoset 1) |^ Z) st
( f is isomorphic & ( for Y being Subset of Z holds f . Y = chi Y,Z ) ) by WAYBEL18:15; :: thesis: verum

end;

end;