deffunc H₁( Real) -> set = I . ($1,0);
A1: for a being Element of [.0,1.] holds H₁(a) in [.0,1.] by FUZNORM1:15;
ex f being UnOp of [.0,1.] st
for a being Element of [.0,1.] holds f . a = H₁(a) from FUNCT_2:sch 8(A1);
hence ex b₁ being UnOp of [.0,1.] st
for x being Element of [.0,1.] holds b₁ . x = I . (x,0) ; :: thesis: verum