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)

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 )
;

end;

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 A1, XBOOLE_0:def 5;

A6: rng (f /^ 1) c= rng (Rotate (f,p1)) by Th101;

A7: f -: p1 <> {} by A2, FINSEQ_5:47;

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:46;

rng f = (rng (f -: p1)) \/ (rng (f :- p1)) by A2, Th70;

then A10: p2 in rng (f :- p1) by A1, A8, XBOOLE_0:def 3;

p1 in rng (f :- p1) by Th61;

then A11: p2 .. (f :- p1) <> 1 by A10, A9, A4, FINSEQ_5:9;

then p2 in rng ((f :- p1) /^ 1) by A10, Th78;

then A12: p2 in (rng ((f :- p1) /^ 1)) \ (rng ((f -: p1) /^ 1)) by A5, XBOOLE_0:def 5;

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, Th64

.= ((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 A10, Th66

.= ((f :- p2) ^ ((f -: p1) /^ 1)) ^ (((f :- p1) /^ 1) -: p2) by A10, A11, Th60

.= (f :- p2) ^ (((f -: p1) /^ 1) ^ (((f :- p1) /^ 1) -: p2)) by FINSEQ_1:32

.= (f :- p2) ^ ((((f -: p1) /^ 1) ^ ((f :- p1) /^ 1)) -: p2) by A12, Th67

.= (f :- p2) ^ ((((f -: p1) ^ ((f :- p1) /^ 1)) /^ 1) -: p2) by A7, Th77

.= (f :- p2) ^ ((f /^ 1) -: p2) by A2, Th76

.= (f :- p2) ^ ((f -: p2) /^ 1) by A1, A13, Th60

.= Rotate (f,p2) by A1, Def2 ;

:: thesis: verum

end;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 A1, XBOOLE_0:def 5;

A6: rng (f /^ 1) c= rng (Rotate (f,p1)) by Th101;

A7: f -: p1 <> {} by A2, FINSEQ_5:47;

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:46;

rng f = (rng (f -: p1)) \/ (rng (f :- p1)) by A2, Th70;

then A10: p2 in rng (f :- p1) by A1, A8, XBOOLE_0:def 3;

p1 in rng (f :- p1) by Th61;

then A11: p2 .. (f :- p1) <> 1 by A10, A9, A4, FINSEQ_5:9;

then p2 in rng ((f :- p1) /^ 1) by A10, Th78;

then A12: p2 in (rng ((f :- p1) /^ 1)) \ (rng ((f -: p1) /^ 1)) by A5, XBOOLE_0:def 5;

A13: now :: thesis: not p2 .. f = 1

then
p2 in rng (f /^ 1)
by A1, Th78;assume
p2 .. f = 1
; :: thesis: contradiction

then p2 .. f <= p1 .. f by A2, FINSEQ_4:21;

hence contradiction by A1, A2, A8, FINSEQ_5:46; :: thesis: verum

end;then p2 .. f <= p1 .. f by A2, FINSEQ_4:21;

hence contradiction by A1, A2, A8, FINSEQ_5:46; :: thesis: verum

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, Th64

.= ((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 A10, Th66

.= ((f :- p2) ^ ((f -: p1) /^ 1)) ^ (((f :- p1) /^ 1) -: p2) by A10, A11, Th60

.= (f :- p2) ^ (((f -: p1) /^ 1) ^ (((f :- p1) /^ 1) -: p2)) by FINSEQ_1:32

.= (f :- p2) ^ ((((f -: p1) /^ 1) ^ ((f :- p1) /^ 1)) -: p2) by A12, Th67

.= (f :- p2) ^ ((((f -: p1) ^ ((f :- p1) /^ 1)) /^ 1) -: p2) by A7, Th77

.= (f :- p2) ^ ((f /^ 1) -: p2) by A2, Th76

.= (f :- p2) ^ ((f -: p2) /^ 1) by A1, A13, Th60

.= Rotate (f,p2) by A1, Def2 ;

:: thesis: verum