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