let X, Y, Z be set ; :: thesis: Funcs ((X --> Y),Z) = X --> (Funcs (Y,Z))
A1: X = dom (X --> Y) by FUNCOP_1:13;

A2: now

let x be set ; :: thesis: ( x in X implies (Funcs ((X --> Y),Z)) . x = Funcs (Y,Z) )
assume A3: x in X ; :: thesis: (Funcs ((X --> Y),Z)) . x = Funcs (Y,Z)
then (Funcs ((X --> Y),Z)) . x = Funcs (((X --> Y) . x),Z) by A1, Def8;
hence (Funcs ((X --> Y),Z)) . x = Funcs (Y,Z) by A3, FUNCOP_1:7; :: thesis: verum

end;

dom (Funcs ((X --> Y),Z)) = dom (X --> Y) by Def8;
hence Funcs ((X --> Y),Z) = X --> (Funcs (Y,Z)) by A1, A2, FUNCOP_1:11; :: thesis: verum