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