let e be Element of SetVal (V,(p => (q => r))); :: thesis: e is Function-yielding
let x be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in dom e or e . x is set )
assume x in dom e ; :: thesis: e . x is set
e in SetVal (V,(p => (q => r))) ;
then e in Funcs ((SetVal (V,p)),(SetVal (V,(q => r)))) by Def2;
then e is Function of (SetVal (V,p)),(SetVal (V,(q => r))) by FUNCT_2:66;
hence e . x is set ; :: thesis: verum