let F, G be Function of X,D; :: thesis: ( ( for p being Element of X holds p in F . p ) & ( for p being Element of X holds p in G . p ) implies F = G )
assume A4: ( ( for p being Element of X holds p in F . p ) & ( for p being Element of X holds p in G . p ) ) ; :: thesis: F = G

now :: thesis: for x being Element of X holds F . x = G . x

let x be Element of X; :: thesis: F . x = G . x
( x in F . x & x in G . x ) by A4;
then A5: not F . x misses G . x by XBOOLE_0:3;
( F . x is Subset of X & G . x is Subset of X ) by TARSKI:def 3;
hence F . x = G . x by A5, Def4; :: thesis: verum

end;

hence F = G by FUNCT_2:63; :: thesis: verum