let X, Y be set ; :: thesis: Funcs X,<*Y*> = <*(Funcs X,Y)*>
A1: ( dom (Funcs X,<*Y*>) = dom <*Y*> & dom <*Y*> = Seg 1 & <*Y*> . 1 = Y ) by Def9, 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, Def9;
hence Funcs X,<*Y*> = <*(Funcs X,Y)*> by A1, FINSEQ_1:def 8; :: thesis: verum