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