thus ex U being UnOp of (V .. W) st
for S1 being Element of V .. W holds U . S1 = H₁(S1) from FUNCT_2:sch 4(); :: thesis: verum