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

A2: now :: thesis: for x being object st x in Y holds
(Funcs (X,(Y --> Z))) . x = Funcs (X,Z)

let x be object ; :: 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, Def8;
hence (Funcs (X,(Y --> Z))) . x = Funcs (X,Z) by A3, FUNCOP_1:7; :: thesis: verum

end;

dom (Funcs (X,(Y --> Z))) = dom (Y --> Z) by Def8;
hence Funcs (X,(Y --> Z)) = Y --> (Funcs (X,Z)) by A2, FUNCOP_1:11; :: thesis: verum