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