let f, g be Function; :: thesis: ( dom f = (dom f1) /\ (dom f2) & ( for c being object st c in dom f holds
f . c = (f1 . c) + (f2 . c) ) & dom g = (dom f1) /\ (dom f2) & ( for c being object st c in dom g holds
g . c = (f1 . c) + (f2 . c) ) implies f = g )
assume that
A1: dom f = (dom f1) /\ (dom f2) and
A2: for c being object st c in dom f holds
f . c = H₁(c) and
A3: dom g = (dom f1) /\ (dom f2) and
A4: for c being object st c in dom g holds
g . c = H₁(c) ; :: thesis: f = g

now :: thesis: for x being object st x in dom f holds
f . x = g . x

let x be object ; :: thesis: ( x in dom f implies f . x = g . x )
assume A5: x in dom f ; :: thesis: f . x = g . x
hence f . x = H₁(x) by A2
.= g . x by A1, A3, A4, A5 ;
:: thesis: verum

end;

hence f = g by A1, A3; :: thesis: verum