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 1) |^ Z = RelStr(# {{} },(id {{} }) #) by YELLOW_1:27;
A3: InclPoset (bool {} ) = RelStr(# (bool {} ),(RelIncl (bool {} )) #) by YELLOW_1:def 1;
A4: BoolePoset Z = InclPoset (bool {} ) by A1, YELLOW_1:4;
then reconsider f = id {{} } as Function of (BoolePoset Z),((BoolePoset 1) |^ Z) by A3, A1, YELLOW_1:27, ZFMISC_1:1;
take f ; :: thesis: ( f is isomorphic & ( for Y being Subset of Z holds f . Y = chi Y,Z ) )
A5: rng (id {{} }) = {{} } by RELAT_1:71;
for x, y being Element of (BoolePoset Z) holds
( x <= y iff f . x <= f . y ) by A4, A3;
hence f is isomorphic by A2, A5, 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 = {} by A1, FUNCT_1:35;
hence f . Y = chi Y,Z by A1; :: 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 Z9 = Z as non empty set ;
(BoolePoset 1) |^ Z = product (Z9 --> (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;