deffunc H₁( Element of CNS) -> Element of REAL = ||.(f /. $1).||;
defpred S₁[ set ] means $1 in dom f;
consider F being PartFunc of the carrier of CNS,REAL such that
A1: for c being Element of CNS holds
( c in dom F iff S₁[c] ) and
A2: for c being Element of CNS st c in dom F holds
F . c = H₁(c) from SEQ_1:sch 3();
reconsider F = F as PartFunc of the carrier of CNS,REAL ;
take F ; :: thesis: ( dom F = dom f & ( for c being Point of CNS st c in dom F holds
F . c = ||.(f /. c).|| ) )
thus dom F = dom f by A1, SUBSET_1:8; :: thesis: for c being Point of CNS st c in dom F holds
F . c = ||.(f /. c).||
thus for c being Point of CNS st c in dom F holds
F . c = ||.(f /. c).|| by A2; :: thesis: verum