let H1, H2 be Function of X,(Y + Z); :: thesis: ( ( for x being Element of X holds H1 . x = (F . x) + (G . x) ) & ( for x being Element of X holds H2 . x = (F . x) + (G . x) ) implies H1 = H2 )

assume that

A4: for x being Element of X holds H1 . x = (F . x) + (G . x) and

A5: for x being Element of X holds H2 . x = (F . x) + (G . x) ; :: thesis: H1 = H2

for x being object st x in X holds

H1 . x = H2 . x

assume that

A4: for x being Element of X holds H1 . x = (F . x) + (G . x) and

A5: for x being Element of X holds H2 . x = (F . x) + (G . x) ; :: thesis: H1 = H2

for x being object st x in X holds

H1 . x = H2 . x

proof

hence
H1 = H2
by FUNCT_2:12; :: thesis: verum
let x be object ; :: thesis: ( x in X implies H1 . x = H2 . x )

assume x in X ; :: thesis: H1 . x = H2 . x

then reconsider x = x as Element of X ;

H1 . x = (F . x) + (G . x) by A4

.= H2 . x by A5 ;

hence H1 . x = H2 . x ; :: thesis: verum

end;assume x in X ; :: thesis: H1 . x = H2 . x

then reconsider x = x as Element of X ;

H1 . x = (F . x) + (G . x) by A4

.= H2 . x by A5 ;

hence H1 . x = H2 . x ; :: thesis: verum