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