let D be non empty set ; :: thesis: for p1, p2 being Element of D
for f being FinSequence of D st p2 .. f <> 1 & 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 .. f <> 1 & p2 in (rng f) \ (rng (f :- p1)) holds
Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)

let f be FinSequence of D; :: thesis: ( p2 .. f <> 1 & p2 in (rng f) \ (rng (f :- p1)) implies Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) )
assume that
A1: p2 .. f <> 1 and
A2: 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 A3: p1 in rng f ; :: thesis: Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)
then A4: f -: p1 <> {} by FINSEQ_5:47;
A5: not p2 in rng (f :- p1) by ;
rng f = (rng (f -: p1)) \/ (rng (f :- p1)) by ;
then A6: p2 in rng (f -: p1) by ;
(f -: p1) ^ ((f :- p1) /^ 1) = f by ;
then A7: p2 .. (f -: p1) <> 1 by A1, A6, Th6;
then A8: p2 in rng ((f -: p1) /^ 1) by ;
then A9: p2 in (rng ((f -: p1) /^ 1)) \ (rng (f :- p1)) by ;
A10: Rotate (f,p1) = (f :- p1) ^ ((f -: p1) /^ 1) by ;
then rng (Rotate (f,p1)) = (rng (f :- p1)) \/ (rng ((f -: p1) /^ 1)) by FINSEQ_1:31;
then p2 in rng (Rotate (f,p1)) by ;
hence Rotate ((Rotate (f,p1)),p2) = (((f :- p1) ^ ((f -: p1) /^ 1)) :- p2) ^ ((((f :- p1) ^ ((f -: p1) /^ 1)) -: p2) /^ 1) by
.= (((f -: p1) /^ 1) :- p2) ^ ((((f :- p1) ^ ((f -: p1) /^ 1)) -: p2) /^ 1) by
.= (((f -: p1) /^ 1) :- p2) ^ (((f :- p1) ^ (((f -: p1) /^ 1) -: p2)) /^ 1) by
.= (((f -: p1) /^ 1) :- p2) ^ (((f :- p1) /^ 1) ^ (((f -: p1) /^ 1) -: p2)) by Th77
.= ((((f -: p1) /^ 1) :- p2) ^ ((f :- p1) /^ 1)) ^ (((f -: p1) /^ 1) -: p2) by FINSEQ_1:32
.= ((((f -: p1) /^ 1) ^ ((f :- p1) /^ 1)) :- p2) ^ (((f -: p1) /^ 1) -: p2) by
.= ((((f -: p1) ^ ((f :- p1) /^ 1)) /^ 1) :- p2) ^ (((f -: p1) /^ 1) -: p2) by
.= ((f /^ 1) :- p2) ^ (((f -: p1) /^ 1) -: p2) by
.= (f :- p2) ^ (((f -: p1) /^ 1) -: p2) by A1, A2, Th83
.= (f :- p2) ^ (((f -: p1) -: p2) /^ 1) by A6, A7, Th60
.= (f :- p2) ^ ((f -: p2) /^ 1) by A3, A6, Th75
.= 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;