let D be non empty set ; :: thesis: for p1, p2 being Element of D
for f being FinSequence of D st p2 in (rng f) \ (rng (f -: p1)) holds
Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)

let p1, p2 be Element of D; :: thesis: for f being FinSequence of D st p2 in (rng f) \ (rng (f -: p1)) holds
Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)

let f be FinSequence of D; :: thesis: ( p2 in (rng f) \ (rng (f -: p1)) implies Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) )
assume A1: p2 in (rng f) \ (rng (f -: p1)) ; :: thesis: Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)
per cases ( p1 in rng f or not p1 in rng f ) ;
suppose A2: p1 in rng f ; :: thesis: Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)
then A3: Rotate (f,p1) = (f :- p1) ^ ((f -: p1) /^ 1) by Def2;
A4: p1 .. (f :- p1) = 1 by Th79;
rng ((f -: p1) /^ 1) c= rng (f -: p1) by FINSEQ_5:33;
then A5: not p2 in rng ((f -: p1) /^ 1) by ;
A6: rng (f /^ 1) c= rng (Rotate (f,p1)) by Th101;
A7: f -: p1 <> {} by ;
A8: not p2 in rng (f -: p1) by ;
p1 .. f <= p1 .. f ;
then A9: p1 <> p2 by ;
rng f = (rng (f -: p1)) \/ (rng (f :- p1)) by ;
then A10: p2 in rng (f :- p1) by ;
p1 in rng (f :- p1) by Th61;
then A11: p2 .. (f :- p1) <> 1 by ;
then p2 in rng ((f :- p1) /^ 1) by ;
then A12: p2 in (rng ((f :- p1) /^ 1)) \ (rng ((f -: p1) /^ 1)) by ;
A13: now :: thesis: not p2 .. f = 1
assume p2 .. f = 1 ; :: thesis: contradiction
then p2 .. f <= p1 .. f by ;
hence contradiction by A1, A2, A8, FINSEQ_5:46; :: thesis: verum
end;
then p2 in rng (f /^ 1) by ;
hence Rotate ((Rotate (f,p1)),p2) = (((f :- p1) ^ ((f -: p1) /^ 1)) :- p2) ^ ((((f :- p1) ^ ((f -: p1) /^ 1)) -: p2) /^ 1) by A3, A6, Def2
.= (((f :- p1) :- p2) ^ ((f -: p1) /^ 1)) ^ ((((f :- p1) ^ ((f -: p1) /^ 1)) -: p2) /^ 1) by
.= ((f :- p2) ^ ((f -: p1) /^ 1)) ^ ((((f :- p1) ^ ((f -: p1) /^ 1)) -: p2) /^ 1) by A1, A2, Th71
.= ((f :- p2) ^ ((f -: p1) /^ 1)) ^ (((f :- p1) -: p2) /^ 1) by
.= ((f :- p2) ^ ((f -: p1) /^ 1)) ^ (((f :- p1) /^ 1) -: p2) by
.= (f :- p2) ^ (((f -: p1) /^ 1) ^ (((f :- p1) /^ 1) -: p2)) by FINSEQ_1:32
.= (f :- p2) ^ ((((f -: p1) /^ 1) ^ ((f :- p1) /^ 1)) -: p2) by
.= (f :- p2) ^ ((((f -: p1) ^ ((f :- p1) /^ 1)) /^ 1) -: p2) by
.= (f :- p2) ^ ((f /^ 1) -: p2) by
.= (f :- p2) ^ ((f -: p2) /^ 1) by
.= Rotate (f,p2) by ;
:: thesis: verum
end;
suppose not p1 in rng f ; :: thesis: Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)
hence Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) by Def2; :: thesis: verum
end;
end;