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

proof

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;

hence H1 = H2 by FUNCT_2:12; :: thesis: verum