deffunc H₁( Complex) -> Element of COMPLEX = In ((1r * c₁),COMPLEX);
defpred S₁[ set ] means c₁ in COMPLEX ;
consider f being PartFunc of COMPLEX,COMPLEX such that
A1: ( ( for a being Element of COMPLEX holds
( a in dom f iff S₁[a] ) ) & ( for a being Element of COMPLEX st a in dom f holds
f . a = H₁(a) ) ) from SEQ_1:sch 3();
take f ; :: thesis: ( f is total & f is linear )
for y being object st y in COMPLEX holds
y in dom f by A1;
then COMPLEX c= dom f ;
then A2: dom f = COMPLEX ;
hence f is total by PARTFUN1:def 2; :: thesis: f is linear
take 1r ; :: according to CFDIFF_1:def 4 :: thesis: for z being Complex holds f /. z = 1r * z
let z be Complex; :: thesis: f /. z = 1r * z
reconsider z = z as Element of COMPLEX by XCMPLX_0:def 2;
f /. z = f . z by A2, PARTFUN1:def 6
.= H₁(z) by A1 ;
hence f /. z = 1r * z ; :: thesis: verum