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 RELAT_1:def 19;
hence <:f,X,Y:> = f by Th85; :: thesis: verum