let A, B be set ; :: thesis: ( ( X <> {} & ( for x being Function st x in X holds
A = dom x ) & ( for x being Function st x in X holds
B = dom x ) implies A = B ) & ( not X <> {} & A = {} & B = {} implies A = B ) )
thus ( X <> {} & ( for x being Function st x in X holds
A = dom x ) & ( for x being Function st x in X holds
B = dom x ) implies A = B ) :: thesis: ( not X <> {} & A = {} & B = {} implies A = B )

proof

assume A2: X <> {} ; :: thesis: ( ex x being Function st
( x in X & not A = dom x ) or ex x being Function st
( x in X & not B = dom x ) or A = B )
assume that
A3: for x being Function st x in X holds
A = dom x and
A4: for x being Function st x in X holds
B = dom x ; :: thesis: A = B
consider x being set such that
A5: x in X by A2, XBOOLE_0:def 1;
reconsider x = x as Function by A5;
( A = dom x & B = dom x ) by A3, A4, A5;
hence A = B ; :: thesis: verum

end;

thus ( not X <> {} & A = {} & B = {} implies A = B ) ; :: thesis: verum