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

A2: now :: thesis: for x being object st x in X holds
(Funcs ((X --> Y),Z)) . x = Funcs (Y,Z)

let x be object ; :: 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, Def7;
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 Def7;
hence Funcs ((X --> Y),Z) = X --> (Funcs (Y,Z)) by A2, FUNCOP_1:11; :: thesis: verum