let D be non empty set ; :: thesis: for n being non empty 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 empty 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
A20: len s = n by CARD_1:def 7;
then 1 <= len s by NAT_1:14;
then ( Op-RightShift s is FinSequence of D & len (Op-RightShift s) = len s ) by LM004A;
then Op-RightShift s is Tuple of n,D by A20, CARD_1:def 7;
hence Op-RightShift s is Element of n -tuples_on D by FINSEQ_2:131; :: thesis: verum