let D be non empty set ; :: thesis: for n being non zero Element of NAT
for s being Element of n -tuples_on D holds Op-RightShift s is Element of n -tuples_on D
let n be non zero Element of NAT ; :: thesis: for s being Element of n -tuples_on D holds Op-RightShift s is Element of n -tuples_on D
let s be Element of n -tuples_on D; :: thesis: Op-RightShift s is Element of n -tuples_on D
A1: len s = n by CARD_1:def 7;
( Op-RightShift s is FinSequence of D & len (Op-RightShift s) = len s ) by Th8, Th7, NAT_1:14;
then Op-RightShift s is Tuple of n,D by A1, CARD_1:def 7;
hence Op-RightShift s is Element of n -tuples_on D by FINSEQ_2:131; :: thesis: verum