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

now

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

end;

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