consider F being PartFunc of Z,(REAL n) such that
A3: for c being Element of Z holds
( c in dom F iff S₁[c] ) and
A4: for c being Element of Z st c in dom F holds
F /. c = H₁(c) from PARTFUN2:sch 2();
take F ; :: thesis: ( dom F = dom f & ( for c being set st c in dom F holds
F /. c = - (f /. c) ) )
thus ( dom F = dom f & ( for c being set st c in dom F holds
F /. c = - (f /. c) ) ) by A3, A4, SUBSET_1:3; :: thesis: verum