let i, n be Element of NAT ; 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 ; ( 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
; 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; Del (p,i) in n -tuples_on D
A3:
len p = n + 1
by CARD_1:def 7;
then
i in dom p
by A1, A2, FINSEQ_3:25;
then A4:
len (Del (p,i)) = n
by A3, FINSEQ_3:109;
Del (p,i) is FinSequence of D
by FINSEQ_3:105;
then
Del (p,i) is Element of n -tuples_on D
by A4, FINSEQ_2:92;
hence
Del (p,i) in n -tuples_on D
; verum