let X, Y, Z be set ; 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; verum