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-LeftShift 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-LeftShift s is Element of n -tuples_on D
let s be Element of n -tuples_on D; :: thesis: Op-LeftShift s is Element of n -tuples_on D
A1: len s = n by CARD_1:def 7;
1 <= len s by NAT_1:14;
then ( Op-LeftShift s is FinSequence of D & len (Op-LeftShift s) = len s ) by Th5;
then Op-LeftShift s is Tuple of n,D by A1, CARD_1:def 7;
hence Op-LeftShift s is Element of n -tuples_on D by FINSEQ_2:131; :: thesis: verum