consider f being Function of the carrier of BL, the carrier of BL such that

A1: for a being Element of BL holds f . a = H_{1}(a)
from FUNCT_2:sch 4();

take f ; :: thesis: for a being Element of BL holds f . a = a `

thus for a being Element of BL holds f . a = a ` by A1; :: thesis: verum

A1: for a being Element of BL holds f . a = H

take f ; :: thesis: for a being Element of BL holds f . a = a `

thus for a being Element of BL holds f . a = a ` by A1; :: thesis: verum