let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D holds dom (Rotate (f,p)) = dom f
let p be Element of D; :: thesis: for f being FinSequence of D holds dom (Rotate (f,p)) = dom f
let f be FinSequence of D; :: thesis: dom (Rotate (f,p)) = dom f
len (Rotate (f,p)) = len f by Th14;
hence dom (Rotate (f,p)) = dom f by FINSEQ_3:29; :: thesis: verum