defpred S₁[ set ] means $1 in dom f;
consider F being PartFunc of C,COMPLEX such that
A1: for c being Element of C holds
( c in dom F iff S₁[c] ) and
A2: for c being Element of C st c in dom F holds
F . c = H₁(c) from SEQ_1:sch 3();
take F ; :: thesis: ( dom F = dom f & ( for c being Element of C st c in dom F holds
F . c = (f /. c) *' ) )
thus dom f = dom F by A1, SUBSET_1:8; :: thesis: for c being Element of C st c in dom F holds
F . c = (f /. c) *'
thus for c being Element of C st c in dom F holds
F . c = (f /. c) *' by A2; :: thesis: verum