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