let p be Point of (TOP-REAL 2); :: thesis: for f being V8() standard special_circular_sequence holds Rev (Rotate f,p) = Rotate (Rev f),p
let f be V8() standard special_circular_sequence; :: thesis: Rev (Rotate f,p) = Rotate (Rev f),p

per cases ( not p in rng f or p = f /. 1 or ( p in rng f & p <> f /. 1 ) ) ;

suppose A1: not p in rng f ; :: thesis: Rev (Rotate f,p) = Rotate (Rev f),p

then A2: Rotate f,p = f by FINSEQ_6:def 2;
not p in rng (Rev f) by A1, FINSEQ_5:60;
hence Rev (Rotate f,p) = Rotate (Rev f),p by A2, FINSEQ_6:def 2; :: thesis: verum

end;

suppose A3: p = f /. 1 ; :: thesis: Rev (Rotate f,p) = Rotate (Rev f),p

then A4: Rotate f,p = f by FINSEQ_6:95;
p = (Rev f) /. (len f) by A3, FINSEQ_5:68
.= (Rev f) /. (len (Rev f)) by FINSEQ_5:def 3
.= (Rev f) /. 1 by FINSEQ_6:def 1 ;
hence Rev (Rotate f,p) = Rotate (Rev f),p by A4, FINSEQ_6:95; :: thesis: verum

end;

suppose that A5: p in rng f and
A6: p <> f /. 1 ; :: thesis: Rev (Rotate f,p) = Rotate (Rev f),p

f just_once_values p

proof

take p .. f ; :: according to REVROT_1:def 2 :: thesis: ( p .. f in dom f & p = f /. (p .. f) & ( for z being set st z in dom f & z <> p .. f holds
f /. z <> p ) )
thus A7: p .. f in dom f by A5, FINSEQ_4:30; :: thesis: ( p = f /. (p .. f) & ( for z being set st z in dom f & z <> p .. f holds
f /. z <> p ) )
thus A8: p = f . (p .. f) by A5, FINSEQ_4:29
.= f /. (p .. f) by A7, PARTFUN1:def 8 ; :: thesis: for z being set st z in dom f & z <> p .. f holds
f /. z <> p
let z be set ; :: thesis: ( z in dom f & z <> p .. f implies f /. z <> p )
assume that
A9: z in dom f and
A10: z <> p .. f ; :: thesis: f /. z <> p
reconsider k = z as Element of NAT by A9;

per cases ( k < p .. f or k > p .. f ) by A10, XXREAL_0:1;

suppose A11: k < p .. f ; :: thesis: f /. z <> p

A12: p .. f <= len f by A5, FINSEQ_4:31;
p .. f <> len f by A6, A8, FINSEQ_6:def 1;
then A13: p .. f < len f by A12, XXREAL_0:1;
1 <= k by A9, FINSEQ_3:27;
hence f /. z <> p by A8, A11, A13, GOBOARD7:38; :: thesis: verum

end;

suppose A14: k > p .. f ; :: thesis: f /. z <> p

p .. f >= 1 by A5, FINSEQ_4:31;
then A15: p .. f > 1 by A6, A8, XXREAL_0:1;
k <= len f by A9, FINSEQ_3:27;
hence f /. z <> p by A8, A14, A15, GOBOARD7:39; :: thesis: verum

end;

end;

end;

hence Rev (Rotate f,p) = Rotate (Rev f),p by FINSEQ_6:112; :: thesis: verum

end;

end;