let D be non empty set ; :: thesis: for f being FinSequence of D st f is poorly-one-to-one & f is circular holds
for p being Element of D holds Rotate (f,p) is poorly-one-to-one
let f be FinSequence of D; :: thesis: ( f is poorly-one-to-one & f is circular implies for p being Element of D holds Rotate (f,p) is poorly-one-to-one )
assume A1: ( f is poorly-one-to-one & f is circular ) ; :: thesis: for p being Element of D holds Rotate (f,p) is poorly-one-to-one
let p be Element of D; :: thesis: Rotate (f,p) is poorly-one-to-one
A2: len (Rotate (f,p)) = len f by FINSEQ_6:179;

per cases ( len f <> 2 or len f = 2 ) ;

suppose A3: len f <> 2 ; :: thesis: Rotate (f,p) is poorly-one-to-one

then f is weakly-one-to-one by A1, Th7;
then Rotate (f,p) is weakly-one-to-one by A1, Th12;
hence Rotate (f,p) is poorly-one-to-one by A2, A3, Th7; :: thesis: verum

end;

suppose len f = 2 ; :: thesis: Rotate (f,p) is poorly-one-to-one

hence Rotate (f,p) is poorly-one-to-one by A2, Def3; :: thesis: verum

end;

end;