let X, Y, Z be set ; :: thesis: for f being PartFunc of , holds ~ (~ f) = f
let f be PartFunc of ,; :: thesis: ~ (~ f) = f
dom f c= [:X,Y:] ;
hence ~ (~ f) = f by Th53; :: thesis: verum