reconsider f = UFilter BL as Function ;

A1: dom f = the carrier of BL by Def6;

rng f c= bool (ultraset BL)

for a being Element of BL holds f . a = { F where F is Filter of BL : ( F is being_ultrafilter & a in F ) } by Def6;

hence UFilter BL is Function of the carrier of BL,(bool (ultraset BL)) ; :: thesis: verum

A1: dom f = the carrier of BL by Def6;

rng f c= bool (ultraset BL)

proof

then reconsider f = f as Function of the carrier of BL,(bool (ultraset BL)) by A1, FUNCT_2:def 1, RELSET_1:4;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in bool (ultraset BL) )

reconsider yy = y as set by TARSKI:1;

assume y in rng f ; :: thesis: y in bool (ultraset BL)

then consider x being object such that

A2: x in dom f and

A3: y = f . x by FUNCT_1:def 3;

y = { F where F is Filter of BL : ( F is being_ultrafilter & x in F ) } by A1, A2, A3, Def6;

then yy c= ultraset BL by A1, A2, Th16;

hence y in bool (ultraset BL) ; :: thesis: verum

end;reconsider yy = y as set by TARSKI:1;

assume y in rng f ; :: thesis: y in bool (ultraset BL)

then consider x being object such that

A2: x in dom f and

A3: y = f . x by FUNCT_1:def 3;

y = { F where F is Filter of BL : ( F is being_ultrafilter & x in F ) } by A1, A2, A3, Def6;

then yy c= ultraset BL by A1, A2, Th16;

hence y in bool (ultraset BL) ; :: thesis: verum

for a being Element of BL holds f . a = { F where F is Filter of BL : ( F is being_ultrafilter & a in F ) } by Def6;

hence UFilter BL is Function of the carrier of BL,(bool (ultraset BL)) ; :: thesis: verum