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 that
A1: 1 <= i and
A2: 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
A3: len p = n + 1 by FINSEQ_1:def 18;
then i in dom p by A1, A2, FINSEQ_3:27;
then A4: len (Del (p,i)) = n by A3, FINSEQ_3:118;
Del (p,i) is FinSequence of D by FINSEQ_3:114;
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