deffunc H₁( object ) -> set = { F where F is Filter of L : ( F in F_primeSet L & $1 in F ) } ;
consider f being Function such that
A1: ( dom f = the carrier of L & ( for x being object st x in the carrier of L holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
take f ; :: thesis: for a being Element of L holds
( dom f = the carrier of L & f . a = { F where F is Filter of L : ( F in F_primeSet L & a in F ) } )
thus for a being Element of L holds
( dom f = the carrier of L & f . a = { F where F is Filter of L : ( F in F_primeSet L & a in F ) } ) by A1; :: thesis: verum