let x be set ; :: thesis: for f being Function st x in dom (~ f) holds
ex y, z being set st x = [y,z]
let f be Function; :: thesis: ( x in dom (~ f) implies ex y, z being set st x = [y,z] )
consider X, Y being set such that
A1: dom (~ f) c= [:X,Y:] by FUNCT_4:45;
assume x in dom (~ f) ; :: thesis: ex y, z being set st x = [y,z]
hence ex y, z being set st x = [y,z] by A1, RELAT_1:def 1; :: thesis: verum