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