deffunc H_{1}( object ) -> set = { F where F is Filter of BL : ( F is being_ultrafilter & $1 in F ) } ;

consider f being Function such that

A1: dom f = the carrier of BL and

A2: for x being object st x in the carrier of BL holds

f . x = H_{1}(x)
from FUNCT_1:sch 3();

take f ; :: thesis: ( dom f = the carrier of BL & ( for a being Element of BL holds f . a = { UF where UF is Filter of BL : ( UF is being_ultrafilter & a in UF ) } ) )

thus ( dom f = the carrier of BL & ( for a being Element of BL holds f . a = { UF where UF is Filter of BL : ( UF is being_ultrafilter & a in UF ) } ) ) by A1, A2; :: thesis: verum

consider f being Function such that

A1: dom f = the carrier of BL and

A2: for x being object st x in the carrier of BL holds

f . x = H

take f ; :: thesis: ( dom f = the carrier of BL & ( for a being Element of BL holds f . a = { UF where UF is Filter of BL : ( UF is being_ultrafilter & a in UF ) } ) )

thus ( dom f = the carrier of BL & ( for a being Element of BL holds f . a = { UF where UF is Filter of BL : ( UF is being_ultrafilter & a in UF ) } ) ) by A1, A2; :: thesis: verum