let X, Y be set ; :: thesis: Funcs <*X*>,Y = <*(Funcs X,Y)*>
A1: dom <*X*> = Seg 1 by FINSEQ_1:def 8;
A2: dom (Funcs <*X*>,Y) = dom <*X*> by Def8;
then reconsider p = Funcs <*X*>,Y as FinSequence by A1, FINSEQ_1:def 2;
( <*X*> . 1 = X & 1 in Seg 1 ) by FINSEQ_1:4, FINSEQ_1:def 8, TARSKI:def 1;
then p . 1 = Funcs X,Y by A1, Def8;
hence Funcs <*X*>,Y = <*(Funcs X,Y)*> by A2, A1, FINSEQ_1:def 8; :: thesis: verum