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