let h1, h2 be Function of (Maps V),V; :: thesis: ( ( for m being Element of Maps V holds h1 . m = dom m ) & ( for m being Element of Maps V holds h2 . m = dom m ) implies h1 = h2 )

assume that

A1: for m being Element of Maps V holds h1 . m = dom m and

A2: for m being Element of Maps V holds h2 . m = dom m ; :: thesis: h1 = h2

assume that

A1: for m being Element of Maps V holds h1 . m = dom m and

A2: for m being Element of Maps V holds h2 . m = dom m ; :: thesis: h1 = h2

now :: thesis: for m being Element of Maps V holds h1 . m = h2 . m

hence
h1 = h2
by FUNCT_2:63; :: thesis: verumlet m be Element of Maps V; :: thesis: h1 . m = h2 . m

thus h1 . m = dom m by A1

.= h2 . m by A2 ; :: thesis: verum

end;thus h1 . m = dom m by A1

.= h2 . m by A2 ; :: thesis: verum