let D be non empty set ; :: thesis: for p2, p1 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 p2, p1 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 Th84;
rng ((f -: p1) /^ 1) c= rng (f -: p1) by FINSEQ_5:36;
then A5: not p2 in rng ((f -: p1) /^ 1) by A1, XBOOLE_0:def 5;
A6: rng (f /^ 1) c= rng (Rotate f,p1) by Th107;
A7: f -: p1 <> {} by A2, FINSEQ_5:50;
A8: not p2 in rng (f -: p1) by A1, XBOOLE_0:def 5;
p1 .. f <= p1 .. f ;
then A9: p1 <> p2 by A2, A8, FINSEQ_5:49;
rng f = (rng (f -: p1)) \/ (rng (f :- p1)) by A2, Th75;
then A10: p2 in rng (f :- p1) by A1, A8, XBOOLE_0:def 3;
p1 in rng (f :- p1) by Th66;
then A11: p2 .. (f :- p1) <> 1 by A10, A9, A4, FINSEQ_5:10;
then p2 in rng ((f :- p1) /^ 1) by A10, Th83;
then A12: p2 in (rng ((f :- p1) /^ 1)) \ (rng ((f -: p1) /^ 1)) by A5, XBOOLE_0:def 5;

A13: now

assume p2 .. f = 1 ; :: thesis: contradiction
then p2 .. f <= p1 .. f by A2, FINSEQ_4:31;
hence contradiction by A1, A2, A8, FINSEQ_5:49; :: thesis: verum

end;

then p2 in rng (f /^ 1) by A1, Th83;
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 A10, Th69
.= ((f :- p2) ^ ((f -: p1) /^ 1)) ^ ((((f :- p1) ^ ((f -: p1) /^ 1)) -: p2) /^ 1) by A1, A2, Th76
.= ((f :- p2) ^ ((f -: p1) /^ 1)) ^ (((f :- p1) -: p2) /^ 1) by A10, Th71
.= ((f :- p2) ^ ((f -: p1) /^ 1)) ^ (((f :- p1) /^ 1) -: p2) by A10, A11, Th65
.= (f :- p2) ^ (((f -: p1) /^ 1) ^ (((f :- p1) /^ 1) -: p2)) by FINSEQ_1:45
.= (f :- p2) ^ ((((f -: p1) /^ 1) ^ ((f :- p1) /^ 1)) -: p2) by A12, Th72
.= (f :- p2) ^ ((((f -: p1) ^ ((f :- p1) /^ 1)) /^ 1) -: p2) by A7, Th82
.= (f :- p2) ^ ((f /^ 1) -: p2) by A2, Th81
.= (f :- p2) ^ ((f -: p2) /^ 1) by A1, A13, Th65
.= Rotate f,p2 by A1, Def2 ;
:: 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;