let i, n be Element of NAT ; :: thesis: for D being non empty set st 1 <= i & i <= n + 1 holds
for p being Element of (n + 1) -tuples_on D holds Del p,i in n -tuples_on D
let D be non empty set ; :: thesis: ( 1 <= i & i <= n + 1 implies for p being Element of (n + 1) -tuples_on D holds Del p,i in n -tuples_on D )
set X = D;
assume A1: ( 1 <= i & i <= n + 1 ) ; :: thesis: for p being Element of (n + 1) -tuples_on D holds Del p,i in n -tuples_on D
let p be Element of (n + 1) -tuples_on D; :: thesis: Del p,i in n -tuples_on D
A2: len p = n + 1 by FINSEQ_2:109;
then A3: i in dom p by A1, FINSEQ_3:27;
A4: Del p,i is FinSequence of D by FINSEQ_3:114;
len (Del p,i) = n by A2, A3, FINSEQ_3:118;
then Del p,i is Element of n -tuples_on D by A4, FINSEQ_2:110;
hence Del p,i in n -tuples_on D ; :: thesis: verum