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