let D be non empty set ; :: thesis: for n being non zero Element of NAT
for m being Integer
for s being Element of n -tuples_on D holds Op-Shift (s,m) is Element of n -tuples_on D
let n be non zero Element of NAT ; :: thesis: for m being Integer
for s being Element of n -tuples_on D holds Op-Shift (s,m) is Element of n -tuples_on D
let m be Integer; :: thesis: for s being Element of n -tuples_on D holds Op-Shift (s,m) is Element of n -tuples_on D
let s be Element of n -tuples_on D; :: thesis: Op-Shift (s,m) is Element of n -tuples_on D
A1: len s = n by CARD_1:def 7;
1 <= len s by NAT_1:14;
then len (Op-Shift (s,m)) = len s by Def3;
then Op-Shift (s,m) is Tuple of n,D by A1, CARD_1:def 7;
hence Op-Shift (s,m) is Element of n -tuples_on D by FINSEQ_2:131; :: thesis: verum