let D be non empty set ; :: thesis: for x1, x2, x3, x4, x5 being Element of D holds <*x1,x2,x3,x4,x5*> is Element of 5 -tuples_on D
let x1, x2, x3, x4, x5 be Element of D; :: thesis: <*x1,x2,x3,x4,x5*> is Element of 5 -tuples_on D
reconsider x12345 = <*x1,x2,x3,x4,x5*> as FinSequence of D ;
P1: len x12345 = 5 by FINSEQ_4:78;
x12345 in D * by FINSEQ_1:def 11;
then x12345 in 5 -tuples_on D by P1;
hence <*x1,x2,x3,x4,x5*> is Element of 5 -tuples_on D ; :: thesis: verum