let x be object ; :: thesis: for f being Function st x in dom (~ f) holds
ex y, z being object st x = [y,z]
let f be Function; :: thesis: ( x in dom (~ f) implies ex y, z being object st x = [y,z] )
assume A1: x in dom (~ f) ; :: thesis: 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; :: thesis: verum