let Z be set ; ex f being Function of (BoolePoset Z),((BoolePoset {0}) |^ 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 = {}
;
ex f being Function of (BoolePoset Z),((BoolePoset {0}) |^ Z) st
( f is isomorphic & ( for Y being Subset of Z holds f . Y = chi (Y,Z) ) )then A2:
(BoolePoset {0}) |^ 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 {0}) |^ Z) by A3, A1, YELLOW_1:27, ZFMISC_1:1;
take
f
;
( f is isomorphic & ( for Y being Subset of Z holds f . Y = chi (Y,Z) ) )A5:
rng (id {{}}) = {{}}
;
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;
for Y being Subset of Z holds f . Y = chi (Y,Z)let Y be
Subset of
Z;
f . Y = chi (Y,Z)
Y = {}
by A1;
then
Y in {{}}
by TARSKI:def 1;
then
f . Y = {}
by A1, FUNCT_1:18;
hence
f . Y = chi (
Y,
Z)
by A1;
verum end;