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