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

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