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
thus <:f,X,Y:> = f ; :: thesis: verum