let X, Y be set ; :: thesis: Funcs X,Y = product (X --> Y)
set f = X --> Y;
A1: dom (X --> Y) = X by 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 and
A3: dom g = X and
A4: 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 A5: y in dom (X --> Y) ; :: thesis: g . y in (X --> Y) . y
then A6: (X --> Y) . y = Y by FUNCOP_1:13;
g . y in rng g by A3, A5, FUNCT_1:def 5;
hence g . y in (X --> Y) . y by A4, A6; :: thesis: verum

end;

hence x in product (X --> Y) by A1, A2, A3, 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
A7: x = g and
A8: dom g = dom (X --> Y) and
A9: 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
A10: z in dom g and
A11: y = g . z by FUNCT_1:def 5;
y in (X --> Y) . z by A8, A9, A10, A11;
hence y in Y by A8, A10, FUNCOP_1:13; :: thesis: verum

end;

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