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 )
proof
A3: dom p = Seg 3 by A1, FINSEQ_1:def 3;
then p . 1 in rng p by FUNCT_1:3, FINSEQ_1:1;
hence <*(p . 1)*> in 1 -tuples_on D by A0, FINSEQ_2:98; :: thesis: ( <*(p . 2)*> in 1 -tuples_on D & <*(p . 3)*> in 1 -tuples_on D )
p . 2 in rng p by A3, FINSEQ_1:1, FUNCT_1:3;
hence <*(p . 2)*> in 1 -tuples_on D by A0, FINSEQ_2:98; :: thesis: <*(p . 3)*> in 1 -tuples_on D
p . 3 in rng p by A3, FINSEQ_1:1, FUNCT_1:3;
hence <*(p . 3)*> in 1 -tuples_on D by A0, FINSEQ_2:98; :: thesis: verum
end;
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; :: thesis: verum