consider F being PartFunc of C,V such that

A1: for c being Element of C holds

( c in dom F iff S_{1}[c] )
and

A2: for c being Element of C st c in dom F holds

F /. c = H_{1}(c)
from PARTFUN2:sch 2();

take F ; :: thesis: ( dom F = dom f & ( for c being Element of C st c in dom F holds

F /. c = r * (f /. c) ) )

thus ( dom F = dom f & ( for c being Element of C st c in dom F holds

F /. c = r * (f /. c) ) ) by A1, A2, SUBSET_1:3; :: thesis: verum

A1: for c being Element of C holds

( c in dom F iff S

A2: for c being Element of C st c in dom F holds

F /. c = H

take F ; :: thesis: ( dom F = dom f & ( for c being Element of C st c in dom F holds

F /. c = r * (f /. c) ) )

thus ( dom F = dom f & ( for c being Element of C st c in dom F holds

F /. c = r * (f /. c) ) ) by A1, A2, SUBSET_1:3; :: thesis: verum