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 FUNCT_6:def 9;
then reconsider p = Funcs (X,<*Y,Z*>) as FinSequence by A1, FINSEQ_1:def 2;
A3: len <*Y,Z*> = 2 by FINSEQ_1:44;
then A4: len p = 2 by A2, A1, FINSEQ_1:def 3;
( <*Y,Z*> . 2 = Z & 2 in Seg 2 ) by FINSEQ_1:2, FINSEQ_1:44, TARSKI:def 2;
then A5: p . 2 = Funcs (X,Z) by A3, A1, FUNCT_6:def 9;
( <*Y,Z*> . 1 = Y & 1 in Seg 2 ) by FINSEQ_1:2, FINSEQ_1:44, TARSKI:def 2;
then p . 1 = Funcs (X,Y) by A3, A1, FUNCT_6:def 9;
hence Funcs (X,<*Y,Z*>) = <*(Funcs (X,Y)),(Funcs (X,Z))*> by A4, A5, FINSEQ_1:44; :: thesis: verum