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