let X be set ; :: thesis: ( ( for f, g being Function st dom f = X & dom g = X holds
f = g ) implies X = {} )
assume A1:
for f, g being Function st dom f = X & dom g = X holds
f = g
; :: thesis: X = {}
consider x being Element of X;
assume A2:
not X = {}
; :: thesis: contradiction
deffunc H1( set ) -> set = {} ;
consider f being Function such that
A3:
dom f = X
and
A4:
for x being set st x in X holds
f . x = H1(x)
from FUNCT_1:sch 3();
deffunc H2( set ) -> set = 1;
consider g being Function such that
A5:
dom g = X
and
A6:
for x being set st x in X holds
g . x = H2(x)
from FUNCT_1:sch 3();
( f . x = {} & g . x = 1 )
by A2, A4, A6;
hence
contradiction
by A1, A3, A5; :: thesis: verum