let e be Element of SetVal V,(p => (q => r)); :: thesis: e is Function-yielding
let x be set ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in proj1 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:121;
hence e . x is set ; :: thesis: verum