consider F being PartFunc of X, the carrier of V such that
A1: for x being Element of X holds
( x in dom F iff S₁[x] ) and
A2: 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 = z * (f /. x) ) )
thus dom F = dom f by A1, SUBSET_1:8; :: thesis: for x being Element of X st x in dom F holds
F /. x = z * (f /. x)
let x be Element of X; :: thesis: ( x in dom F implies F /. x = z * (f /. x) )
assume x in dom F ; :: thesis: F /. x = z * (f /. x)
hence F /. x = z * (f /. x) by A2; :: thesis: verum