set X = dom f;
defpred S₁[ set ] means $1 in dom f;
deffunc H₁( set ) -> Element of REAL = Re (f /. $1);
consider F being PartFunc of COMPLEX ,REAL such that
A1: for z being Complex holds
( z in dom F iff S₁[z] ) and
A2: for z being Complex st z in dom F holds
F . z = H₁(z) from SEQ_1:sch 3();
take F ; :: thesis: ( dom f = dom F & ( for z being Complex st z in dom F holds
F . z = Re (f /. z) ) )
thus dom F = dom f by A1, SUBSET_1:8; :: thesis: for z being Complex st z in dom F holds
F . z = Re (f /. z)
let z be Complex; :: thesis: ( z in dom F implies F . z = Re (f /. z) )
assume z in dom F ; :: thesis: F . z = Re (f /. z)
hence F . z = Re (f /. z) by A2; :: thesis: verum