let X, Y be set ; :: thesis: for f being PartFunc of X,Y holds <:f,X,Y:> = f
let f be PartFunc of X,Y; :: thesis: <:f,X,Y:> = f
( dom f c= X & rng f c= Y ) by RELSET_1:12;
hence <:f,X,Y:> = f by Th85; :: thesis: verum