defpred S₁[ set ] means $1 in dom f;
deffunc H₁( set ) -> Element of REAL = Re (f . $1);
consider F being PartFunc of X,REAL such that
A1: for z being Element of X holds
( z in dom F iff S₁[z] ) and
A2: for z being Element of X st z in dom F holds
F . z = H₁(z) from SEQ_1:sch 3();
take F ; :: thesis: ( dom F = dom f & ( for x being Element of X st x in dom F holds
F . x = Re (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 = Re (f . x)
thus for x being Element of X st x in dom F holds
F . x = Re (f . x) by A2; :: thesis: verum