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

assume that

A3: for m being Element of Maps V holds h1 . m = cod m and

A4: for m being Element of Maps V holds h2 . m = cod m ; :: thesis: h1 = h2

assume that

A3: for m being Element of Maps V holds h1 . m = cod m and

A4: for m being Element of Maps V holds h2 . m = cod 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 = cod m by A3

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

end;thus h1 . m = cod m by A3

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