thus for U1, U2 being UnOp of (V .. W) st ( for S1 being Element of V .. W holds U1 . S1 = H₁(S1) ) & ( for S1 being Element of V .. W holds U2 . S1 = H₁(S1) ) holds
U1 = U2 from LMOD_7:sch 2(); :: thesis: verum