deffunc H₂( set ) -> Element of COMPLEX = In (((f /. $1) "),COMPLEX);
defpred S₁[ set ] means $1 in (dom f) \ (f " {0c});
consider F being PartFunc of C,COMPLEX such that
A1: for c being Element of C holds
( c in dom F iff S₁[c] ) and
A2: for c being Element of C st c in dom F holds
F /. c = H₂(c) from PARTFUN2:sch 2();
take F ; :: thesis: ( dom F = (dom f) \ (f " {0}) & ( for c being Element of C st c in dom F holds
F /. c = (f /. c) " ) )
thus dom F = (dom f) \ (f " {0}) by A1, SUBSET_1:3; :: thesis: for c being Element of C st c in dom F holds
F /. c = (f /. c) "
let c be Element of C; :: thesis: ( c in dom F implies F /. c = (f /. c) " )
assume c in dom F ; :: thesis: F /. c = (f /. c) "
then F /. c = H₂(c) by A2;
hence F /. c = (f /. c) " ; :: thesis: verum