let D be non empty set ; 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; 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,p2)then A4:
f -: p1 <> {}
by FINSEQ_5:47;
A5:
not
p2 in rng (f :- p1)
by A2, XBOOLE_0:def 5;
rng f = (rng (f -: p1)) \/ (rng (f :- p1))
by A3, Th70;
then A6:
p2 in rng (f -: p1)
by A2, A5, XBOOLE_0:def 3;
(f -: p1) ^ ((f :- p1) /^ 1) = f
by A3, Th76;
then A7:
p2 .. (f -: p1) <> 1
by A1, A6, Th6;
then A8:
p2 in rng ((f -: p1) /^ 1)
by A6, Th78;
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:31;
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, Th65
.=
(((f -: p1) /^ 1) :- p2) ^ (((f :- p1) ^ (((f -: p1) /^ 1) -: p2)) /^ 1)
by A9, Th67
.=
(((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 A8, Th64
.=
((((f -: p1) ^ ((f :- p1) /^ 1)) /^ 1) :- p2) ^ (((f -: p1) /^ 1) -: p2)
by A4, Th77
.=
((f /^ 1) :- p2) ^ (((f -: p1) /^ 1) -: p2)
by A3, Th76
.=
(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 A2, Def2
;
verum end;