A0:
rng p c= D
by FINSEQ_1:def 4;
A2:
( <*(p . 1)*> in 1 -tuples_on D & <*(p . 2)*> in 1 -tuples_on D & <*(p . 3)*> in 1 -tuples_on D )
A4:
rng <*<*(p . 1)*>,<*(p . 2)*>,<*(p . 3)*>*> = {<*(p . 1)*>,<*(p . 2)*>,<*(p . 3)*>}
by FINSEQ_2:128;
{<*(p . 1)*>,<*(p . 2)*>,<*(p . 3)*>} c= 1 -tuples_on D
by A2, ENUMSET1:def 1;
hence
<*<*(p . 1)*>,<*(p . 2)*>,<*(p . 3)*>*> is FinSequence of 1 -tuples_on D
by A4, FINSEQ_1:def 4; verum