let D be non empty set ; 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; 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; ( 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))
; 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
;
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;
then
p2 in rng (f /^ 1)
by A1, Th78;
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
;
verum end;