let D be non empty set ; for p2, p1 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 p2, p1 be 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 f be FinSequence of D; ( 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))
; 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
;
Rotate (Rotate f,p1),p2 = Rotate f,p2then A4:
f -: p1 <> {}
by FINSEQ_5:50;
A5:
not
p2 in rng (f :- p1)
by A2, XBOOLE_0:def 5;
rng f = (rng (f -: p1)) \/ (rng (f :- p1))
by A3, Th75;
then A6:
p2 in rng (f -: p1)
by A2, A5, XBOOLE_0:def 3;
(f -: p1) ^ ((f :- p1) /^ 1) = f
by A3, Th81;
then A7:
p2 .. (f -: p1) <> 1
by A1, A6, Th8;
then A8:
p2 in rng ((f -: p1) /^ 1)
by A6, Th83;
then A9:
p2 in (rng ((f -: p1) /^ 1)) \ (rng (f :- p1))
by A5, XBOOLE_0:def 5;
A10:
Rotate f,
p1 = (f :- p1) ^ ((f -: p1) /^ 1)
by A3, Def2;
then
rng (Rotate f,p1) = (rng (f :- p1)) \/ (rng ((f -: p1) /^ 1))
by FINSEQ_1:44;
then
p2 in rng (Rotate f,p1)
by A8, XBOOLE_0:def 3;
hence Rotate (Rotate f,p1),
p2 =
(((f :- p1) ^ ((f -: p1) /^ 1)) :- p2) ^ ((((f :- p1) ^ ((f -: p1) /^ 1)) -: p2) /^ 1)
by A10, Def2
.=
(((f -: p1) /^ 1) :- p2) ^ ((((f :- p1) ^ ((f -: p1) /^ 1)) -: p2) /^ 1)
by A9, Th70
.=
(((f -: p1) /^ 1) :- p2) ^ (((f :- p1) ^ (((f -: p1) /^ 1) -: p2)) /^ 1)
by A9, Th72
.=
(((f -: p1) /^ 1) :- p2) ^ (((f :- p1) /^ 1) ^ (((f -: p1) /^ 1) -: p2))
by Th82
.=
((((f -: p1) /^ 1) :- p2) ^ ((f :- p1) /^ 1)) ^ (((f -: p1) /^ 1) -: p2)
by FINSEQ_1:45
.=
((((f -: p1) /^ 1) ^ ((f :- p1) /^ 1)) :- p2) ^ (((f -: p1) /^ 1) -: p2)
by A8, Th69
.=
((((f -: p1) ^ ((f :- p1) /^ 1)) /^ 1) :- p2) ^ (((f -: p1) /^ 1) -: p2)
by A4, Th82
.=
((f /^ 1) :- p2) ^ (((f -: p1) /^ 1) -: p2)
by A3, Th81
.=
(f :- p2) ^ (((f -: p1) /^ 1) -: p2)
by A1, A2, Th89
.=
(f :- p2) ^ (((f -: p1) -: p2) /^ 1)
by A6, A7, Th65
.=
(f :- p2) ^ ((f -: p2) /^ 1)
by A3, A6, Th80
.=
Rotate f,
p2
by A2, Def2
;
verum end;