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 /^ 1) & f just_once_values p2 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 /^ 1) & f just_once_values p2 holds

Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)

let f be FinSequence of D; :: thesis: ( p2 in rng (f /^ 1) & f just_once_values p2 implies Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) )

for f being FinSequence of D st p2 in rng (f /^ 1) & f just_once_values p2 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 /^ 1) & f just_once_values p2 holds

Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)

let f be FinSequence of D; :: thesis: ( p2 in rng (f /^ 1) & f just_once_values p2 implies Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) )

per cases
( p1 in rng f or not p1 in rng f )
;

end;

suppose A1:
p1 in rng f
; :: thesis: ( p2 in rng (f /^ 1) & f just_once_values p2 implies Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2) )

assume that

A2: p2 in rng (f /^ 1) and

A3: f just_once_values p2 ; :: thesis: Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)

f = ((f -| p1) ^ <*p1*>) ^ (f |-- p1) by A1, FINSEQ_4:51;

then A4: p2 in (rng ((f -| p1) ^ <*p1*>)) \+\ (rng (f |-- p1)) by A3, Th16;

then f = <*(f /. 1)*> ^ (f /^ 1) by FINSEQ_5:29, RELAT_1:38;

then p2 in (rng <*(f /. 1)*>) \+\ (rng (f /^ 1)) by A3, Th16;

then not p2 in rng <*(f /. 1)*> by A2, XBOOLE_0:1;

then not p2 in {(f /. 1)} by FINSEQ_1:39;

then p2 <> f /. 1 by TARSKI:def 1;

then A8: p2 .. f <> 1 by A7, FINSEQ_5:38;

end;A2: p2 in rng (f /^ 1) and

A3: f just_once_values p2 ; :: thesis: Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)

f = ((f -| p1) ^ <*p1*>) ^ (f |-- p1) by A1, FINSEQ_4:51;

then A4: p2 in (rng ((f -| p1) ^ <*p1*>)) \+\ (rng (f |-- p1)) by A3, Th16;

A5: now :: thesis: ( ( p2 in rng ((f -| p1) ^ <*p1*>) & not p2 in rng (f |-- p1) & ( p2 in rng (f :- p1) implies p1 = p2 ) ) or ( not p2 in rng ((f -| p1) ^ <*p1*>) & not p2 in rng (f -: p1) ) )end;

A7:
p2 in rng f
by A3, FINSEQ_4:5;per cases
( ( p2 in rng ((f -| p1) ^ <*p1*>) & not p2 in rng (f |-- p1) ) or not p2 in rng ((f -| p1) ^ <*p1*>) )
by A4, XBOOLE_0:1;

end;

case that
p2 in rng ((f -| p1) ^ <*p1*>)
and

A6: not p2 in rng (f |-- p1) ; :: thesis: ( p2 in rng (f :- p1) implies p1 = p2 )

end;

A6: not p2 in rng (f |-- p1) ; :: thesis: ( p2 in rng (f :- p1) implies p1 = p2 )

now :: thesis: ( ( not p2 in rng <*p1*> & not p2 in rng (f :- p1) ) or ( p2 in rng <*p1*> & p2 = p1 ) )end;

hence
( p2 in rng (f :- p1) implies p1 = p2 )
; :: thesis: verumper cases
( not p2 in rng <*p1*> or p2 in rng <*p1*> )
;

end;

case
not p2 in rng <*p1*>
; :: thesis: not p2 in rng (f :- p1)

then
not p2 in (rng (f |-- p1)) \/ (rng <*p1*>)
by A6, XBOOLE_0:def 3;

then not p2 in rng (<*p1*> ^ (f |-- p1)) by FINSEQ_1:31;

hence not p2 in rng (f :- p1) by A1, Th41; :: thesis: verum

end;then not p2 in rng (<*p1*> ^ (f |-- p1)) by FINSEQ_1:31;

hence not p2 in rng (f :- p1) by A1, Th41; :: thesis: verum

then f = <*(f /. 1)*> ^ (f /^ 1) by FINSEQ_5:29, RELAT_1:38;

then p2 in (rng <*(f /. 1)*>) \+\ (rng (f /^ 1)) by A3, Th16;

then not p2 in rng <*(f /. 1)*> by A2, XBOOLE_0:1;

then not p2 in {(f /. 1)} by FINSEQ_1:39;

then p2 <> f /. 1 by TARSKI:def 1;

then A8: p2 .. f <> 1 by A7, FINSEQ_5:38;

now :: thesis: Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)

hence
Rotate ((Rotate (f,p1)),p2) = Rotate (f,p2)
; :: thesis: verumend;