reconsider f = UFilter BL as Function ;
A1: dom f = the carrier of BL by Def6;
rng f c= bool (ultraset BL)

proof

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;

then reconsider f = f as Function of the carrier of BL,(bool (ultraset BL)) by A1, FUNCT_2:def 1, RELSET_1:4;
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