let X, Y, Z be set ; :: thesis: Funcs X,<*Y,Z*> = <*(Funcs X,Y),(Funcs X,Z)*>
A1: ( len <*Y,Z*> = 2 & dom (Funcs X,<*Y,Z*>) = dom <*Y,Z*> & Seg (len <*Y,Z*>) = dom <*Y,Z*> & <*Y,Z*> . 1 = Y & <*Y,Z*> . 2 = Z ) by Def9, FINSEQ_1:61, FINSEQ_1:def 3;
then reconsider p = Funcs X,<*Y,Z*> as FinSequence by FINSEQ_1:def 2;
( 1 in Seg 2 & 2 in Seg 2 ) by FINSEQ_1:4, TARSKI:def 2;
then ( len p = 2 & p . 1 = Funcs X,Y & p . 2 = Funcs X,Z ) by A1, Def9, FINSEQ_1:def 3;
hence Funcs X,<*Y,Z*> = <*(Funcs X,Y),(Funcs X,Z)*> by FINSEQ_1:61; :: thesis: verum