let X, Y be set ; :: thesis: Funcs X,Y = product (X --> Y)
set f = X --> Y;
A1: ( dom (X --> Y) = X & ( for x being set st x in X holds
(X --> Y) . x = Y ) ) by FUNCOP_1:13, FUNCOP_1:19;
thus Funcs X,Y c= product (X --> Y) :: according to XBOOLE_0:def 10 :: thesis: product (X --> Y) c= Funcs X,Y

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Funcs X,Y or x in product (X --> Y) )
assume x in Funcs X,Y ; :: thesis: x in product (X --> Y)
then consider g being Function such that
A2: ( x = g & dom g = X & rng g c= Y ) by FUNCT_2:def 2;

now

let y be set ; :: thesis: ( y in dom (X --> Y) implies g . y in (X --> Y) . y )
assume y in dom (X --> Y) ; :: thesis: g . y in (X --> Y) . y
then ( (X --> Y) . y = Y & g . y in rng g ) by A2, FUNCOP_1:13, FUNCT_1:def 5;
hence g . y in (X --> Y) . y by A2; :: thesis: verum

end;

hence x in product (X --> Y) by A1, A2, Def5; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in product (X --> Y) or x in Funcs X,Y )
assume x in product (X --> Y) ; :: thesis: x in Funcs X,Y
then consider g being Function such that
A3: ( x = g & dom g = dom (X --> Y) & ( for x being set st x in dom (X --> Y) holds
g . x in (X --> Y) . x ) ) by Def5;
rng g c= Y

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng g or y in Y )
assume y in rng g ; :: thesis: y in Y
then consider z being set such that
A4: ( z in dom g & y = g . z ) by FUNCT_1:def 5;
( y in (X --> Y) . z & (X --> Y) . z = Y ) by A3, A4, FUNCOP_1:13;
hence y in Y ; :: thesis: verum

end;

hence x in Funcs X,Y by A1, A3, FUNCT_2:def 2; :: thesis: verum