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:31; :: thesis: verum