deffunc H₁( Real) -> set = I . ($1,0);
reconsider A = [.0,1.] as non empty real-membered set ;
for o1, o2 being UnOp of A st ( for a being Element of A holds o1 . a = H₁(a) ) & ( for a being Element of A holds o2 . a = H₁(a) ) holds
o1 = o2 from LMOD_7:sch 2();
hence for b₁, b₂ being UnOp of [.0,1.] st ( for x being Element of [.0,1.] holds b₁ . x = I . (x,0) ) & ( for x being Element of [.0,1.] holds b₂ . x = I . (x,0) ) holds
b₁ = b₂ ; :: thesis: verum