let F1, F2 be Function of (Morphs V),V; :: thesis: ( ( for f being Element of Morphs V holds F1 . f = dom f ) & ( for f being Element of Morphs V holds F2 . f = dom f ) implies F1 = F2 )
assume that
A2: for f being Element of Morphs V holds F1 . f = dom f and
A3: for f being Element of Morphs V holds F2 . f = dom f ; :: thesis: F1 = F2

now :: thesis: for f being Element of Morphs V holds F1 . f = F2 . f

let f be Element of Morphs V; :: thesis: F1 . f = F2 . f
F1 . f = dom f by A2;
hence F1 . f = F2 . f by A3; :: thesis: verum

end;

hence F1 = F2 by FUNCT_2:63; :: thesis: verum