let F1, F2 be Function of (Morphs V),V; :: thesis: ( ( for f being Element of Morphs V holds F1 . f = cod f ) & ( for f being Element of Morphs V holds F2 . f = cod f ) implies F1 = F2 )
assume that
A5: for f being Element of Morphs V holds F1 . f = cod f and
A6: for f being Element of Morphs V holds F2 . f = cod 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 = cod f by A5;
hence F1 . f = F2 . f by A6; :: thesis: verum
end;
hence F1 = F2 by FUNCT_2:63; :: thesis: verum