let F, G be Function; :: thesis: ( dom F = (dom f) /\ (dom g) & ( for x being object st x in dom F holds

F . x = (f . x) + (g . x) ) & dom G = (dom f) /\ (dom g) & ( for x being object st x in dom G holds

G . x = (f . x) + (g . x) ) implies F = G )

assume that

A1: dom F = (dom f) /\ (dom g) and

A2: for x being object st x in dom F holds

F . x = H_{1}(x)
and

A3: dom G = (dom f) /\ (dom g) and

A4: for x being object st x in dom G holds

G . x = H_{1}(x)
; :: thesis: F = G

thus dom F = dom G by A1, A3; :: according to FUNCT_1:def 11 :: thesis: for b_{1} being object holds

( not b_{1} in dom F or F . b_{1} = G . b_{1} )

let x be object ; :: thesis: ( not x in dom F or F . x = G . x )

assume A5: x in dom F ; :: thesis: F . x = G . x

hence F . x = H_{1}(x)
by A2

.= G . x by A1, A3, A4, A5 ;

:: thesis: verum

F . x = (f . x) + (g . x) ) & dom G = (dom f) /\ (dom g) & ( for x being object st x in dom G holds

G . x = (f . x) + (g . x) ) implies F = G )

assume that

A1: dom F = (dom f) /\ (dom g) and

A2: for x being object st x in dom F holds

F . x = H

A3: dom G = (dom f) /\ (dom g) and

A4: for x being object st x in dom G holds

G . x = H

thus dom F = dom G by A1, A3; :: according to FUNCT_1:def 11 :: thesis: for b

( not b

let x be object ; :: thesis: ( not x in dom F or F . x = G . x )

assume A5: x in dom F ; :: thesis: F . x = G . x

hence F . x = H

.= G . x by A1, A3, A4, A5 ;

:: thesis: verum