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

now

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

end;

hence Funcs (X --> Y),Z = X --> (Funcs Y,Z) by A1, FUNCOP_1:17; :: thesis: verum