let X, Y, Z be set ; Funcs (X,(Y --> Z)) = Y --> (Funcs (X,Z))
A1:
Y = dom (Y --> Z)
;
A2:
now for x being object st x in Y holds
(Funcs (X,(Y --> Z))) . x = Funcs (X,Z)let x be
object ;
( x in Y implies (Funcs (X,(Y --> Z))) . x = Funcs (X,Z) )assume A3:
x in Y
;
(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;
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; verum