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₁(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