deffunc H₂( set ) -> Element of COMPLEX = In (((f1 /. $1) * ((f2 /. $1) ")),COMPLEX);
defpred S₁[ set ] means $1 in (dom f1) /\ ((dom f2) \ (f2 " {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 f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being Element of C st c in dom F holds
F /. c = (f1 /. c) * ((f2 /. c) ") ) )
thus dom F = (dom f1) /\ ((dom f2) \ (f2 " {0})) by A1, SUBSET_1:3; :: thesis: for c being Element of C st c in dom F holds
F /. c = (f1 /. c) * ((f2 /. c) ")
let c be Element of C; :: thesis: ( c in dom F implies F /. c = (f1 /. c) * ((f2 /. c) ") )
assume c in dom F ; :: thesis: F /. c = (f1 /. c) * ((f2 /. c) ")
then F /. c = H₂(c) by A2;
hence F /. c = (f1 /. c) * ((f2 /. c) ") ; :: thesis: verum