let f1, f2 be Function of X,ExtREAL; :: thesis: ( ( for x being object st x in X holds
( ( x in A implies f1 . x = er ) & ( not x in A implies f1 . x = 0 ) ) ) & ( for x being object st x in X holds
( ( x in A implies f2 . x = er ) & ( not x in A implies f2 . x = 0 ) ) ) implies f1 = f2 )
assume that
A4: for x being object st x in X holds
( ( x in A implies f1 . x = er ) & ( not x in A implies f1 . x = 0 ) ) and
A6: for x being object st x in X holds
( ( x in A implies f2 . x = er ) & ( not x in A implies f2 . x = 0 ) ) ; :: thesis: f1 = f2
for x being object st x in X holds
f1 . x = f2 . x

proof

let x be object ; :: thesis: ( x in X implies f1 . x = f2 . x )
assume A7: x in X ; :: thesis: f1 . x = f2 . x
then A8: ( not x in A implies ( f1 . x = 0 & f2 . x = 0 ) ) by A4, A6;
( x in A implies ( f1 . x = er & f2 . x = er ) ) by A4, A6, A7;
hence f1 . x = f2 . x by A8; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:12; :: thesis: verum