consider F being PartFunc of Z,(REAL n) such that
A3: for c being Element of Z holds
( c in dom F iff S₁[c] ) and
A4: for c being Element of Z st c in dom F holds
F /. c = H₂(c) from PARTFUN2:sch 2();
take F ; :: thesis: ( dom F = (dom f) /\ (dom g) & ( for c being Element of Z st c in dom F holds
F /. c = (f /. c) - (g /. c) ) )
thus dom F = (dom f) /\ (dom g) by A3, SUBSET_1:8; :: thesis: for c being Element of Z st c in dom F holds
F /. c = (f /. c) - (g /. c)
let c be Element of Z; :: thesis: ( c in dom F implies F /. c = (f /. c) - (g /. c) )
assume c in dom F ; :: thesis: F /. c = (f /. c) - (g /. c)
hence F /. c = (f /. c) - (g /. c) by A4; :: thesis: verum