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

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:13; :: 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:17; :: thesis: verum