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

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

hence
F = G
by FUNCT_2:63; :: thesis: verumlet 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;( 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