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

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