let X, Y be set ; 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, FINSEQ_1:def 8, 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; verum