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 A1: 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 A2: e is Function of SetVal V,p, SetVal V,(q => r) by FUNCT_2:121;
then x in SetVal V,p by A1, FUNCT_2:def 1;
then e . x in SetVal V,(q => r) by A2, FUNCT_2:7;
then e . x in Funcs (SetVal V,q),(SetVal V,r) by Def2;
hence e . x is Function ; :: thesis: verum