consider F being PartFunc of X,the carrier of V such that
A3: for x being Element of X holds
( x in dom F iff S₁[x] ) and
A4: for x being Element of X st x in dom F holds
F /. x = H₁(x) from PARTFUN2:sch 2();
take F ; :: thesis: ( dom F = dom f & ( for x being Element of X st x in dom F holds
F /. x = - (f /. x) ) )
thus dom f = dom F by A3, SUBSET_1:8; :: thesis: for x being Element of X st x in dom F holds
F /. x = - (f /. x)
let x be Element of X; :: thesis: ( x in dom F implies F /. x = - (f /. x) )
assume x in dom F ; :: thesis: F /. x = - (f /. x)
hence F /. x = - (f /. x) by A4; :: thesis: verum