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:8; :: thesis: for c being Element of C st c in dom F holds
F /. c = (f1 /. c) * ((f2 /. c) " )
thus for c being Element of C st c in dom F holds
F /. c = (f1 /. c) * ((f2 /. c) " ) by A2; :: thesis: verum