deffunc H₁( Element of COMPLEX ) -> Element of COMPLEX = 1r * c₁;
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 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 set st y in COMPLEX holds
y in dom f by A1;
then COMPLEX c= dom f by TARSKI:def 3;
then A2: dom f = COMPLEX by XBOOLE_0:def 10;
hence f is total by PARTFUN1:def 4; :: 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
thus f /. z = f . z by A2, PARTFUN1:def 8
.= 1r * z by A1, A2 ; :: thesis: verum