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