let D be non trivial set ; :: thesis: for f being non empty FinSequence of D
for g being non trivial FinSequence of D st g /. 1 = f /. (len f) & ( for i being Nat st 1 <= i & i < len f holds
f /. i <> g /. 1 ) holds
Rotate ((f ^' g),(g /. 1)) = g ^' f
let f be non empty FinSequence of D; :: thesis: for g being non trivial FinSequence of D st g /. 1 = f /. (len f) & ( for i being Nat st 1 <= i & i < len f holds
f /. i <> g /. 1 ) holds
Rotate ((f ^' g),(g /. 1)) = g ^' f
let g be non trivial FinSequence of D; :: thesis: ( g /. 1 = f /. (len f) & ( for i being Nat st 1 <= i & i < len f holds
f /. i <> g /. 1 ) implies Rotate ((f ^' g),(g /. 1)) = g ^' f )
assume that
A1: g /. 1 = f /. (len f) and
A2: for i being Nat st 1 <= i & i < len f holds
f /. i <> g /. 1 ; :: thesis: Rotate ((f ^' g),(g /. 1)) = g ^' f
A3: g /. 1 in rng f by A1, FINSEQ_6:168;
A4: len f in dom f by FINSEQ_5:6;
then A5: f . (len f) = f /. (len f) by PARTFUN1:def 6;
for i being Nat st 1 <= i & i < len f holds
f . i <> f . (len f)

proof

let i be Nat; :: thesis: ( 1 <= i & i < len f implies f . i <> f . (len f) )
assume that
A6: 1 <= i and
A7: i < len f ; :: thesis: f . i <> f . (len f)
f . i = f /. i by A6, A7, FINSEQ_4:15;
hence f . i <> f . (len f) by A1, A2, A5, A6, A7; :: thesis: verum

end;

then A8: (g /. 1) .. f = len f by A1, A4, A5, FINSEQ_6:2;
then A9: (f ^' g) :- (g /. 1) = g by Th16;
(f ^' g) -: (g /. 1) = f by A8, Th17;
then A10: ((f ^' g) -: (g /. 1)) /^ 1 = ((1 + 1),(len f)) -cut f by Th13;
rng f c= rng (f ^' g) by Th10;
hence Rotate ((f ^' g),(g /. 1)) = ((f ^' g) :- (g /. 1)) ^ (((f ^' g) -: (g /. 1)) /^ 1) by A3, FINSEQ_6:def 2
.= g ^' f by A9, A10, FINSEQ_6:def 5 ;
:: thesis: verum