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