let X, Y, Z be set ; :: thesis: Funcs <*X,Y*>,Z = <*(Funcs X,Z),(Funcs Y,Z)*>
A1: ( len <*X,Y*> = 2 & dom (Funcs <*X,Y*>,Z) = dom <*X,Y*> & Seg (len <*X,Y*>) = dom <*X,Y*> & <*X,Y*> . 1 = X & <*X,Y*> . 2 = Y ) by Def8, 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,Z & p . 2 = Funcs Y,Z ) by A1, Def8, FINSEQ_1:def 3;
hence Funcs <*X,Y*>,Z = <*(Funcs X,Z),(Funcs Y,Z)*> by FINSEQ_1:61; :: thesis: verum