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

A2: now

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

end;

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