let D1, D2 be set ; :: thesis: ( ( for a being set holds
( a in D1 iff a is Function of VAR ,D ) ) & ( for a being set holds
( a in D2 iff a is Function of VAR ,D ) ) implies D1 = D2 )
assume that
A2: for a being set holds
( a in D1 iff a is Function of VAR ,D ) and
A3: for a being set holds
( a in D2 iff a is Function of VAR ,D ) ; :: thesis: D1 = D2

now

let a be set ; :: thesis: ( ( a in D1 implies a in D2 ) & ( a in D2 implies a in D1 ) )
thus ( a in D1 implies a in D2 ) :: thesis: ( a in D2 implies a in D1 )

proof

assume a in D1 ; :: thesis: a in D2
then a is Function of VAR ,D by A2;
hence a in D2 by A3; :: thesis: verum

end;

assume a in D2 ; :: thesis: a in D1
then a is Function of VAR ,D by A3;
hence a in D1 by A2; :: thesis: verum

end;

hence D1 = D2 by TARSKI:2; :: thesis: verum