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 FUNCT_6:def 8;
then reconsider p = Funcs (<*X*>,Y) as FinSequence by A1, FINSEQ_1:def 2;
( <*X*> . 1 = X & 1 in Seg 1 ) by FINSEQ_1:2, FINSEQ_1:def 8, TARSKI:def 1;
then p . 1 = Funcs (X,Y) by A1, FUNCT_6:def 8;
hence Funcs (<*X*>,Y) = <*(Funcs (X,Y))*> by A2, A1, FINSEQ_1:def 8; :: thesis: verum