let i be Nat; :: thesis: for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & (f /. i) `1 = (f /. (i + 1)) `1 holds
(f /. (i + 1)) `2 = (f /. (i + 2)) `2
let f be FinSequence of the carrier of (TOP-REAL 2); :: thesis: ( f is special & f is alternating & 1 <= i & i + 2 <= len f & (f /. i) `1 = (f /. (i + 1)) `1 implies (f /. (i + 1)) `2 = (f /. (i + 2)) `2 )
assume that
A1: f is special and
A2: ( f is alternating & 1 <= i ) and
A3: i + 2 <= len f ; :: thesis: ( not (f /. i) `1 = (f /. (i + 1)) `1 or (f /. (i + 1)) `2 = (f /. (i + 2)) `2 )
set p2 = f /. (i + 1);
set p3 = f /. (i + 2);
( 1 <= i + 1 & (i + 1) + 1 = i + (1 + 1) ) by NAT_1:11;
then ( (f /. (i + 1)) `1 = (f /. (i + 2)) `1 or (f /. (i + 1)) `2 = (f /. (i + 2)) `2 ) by A1, A3;
hence ( not (f /. i) `1 = (f /. (i + 1)) `1 or (f /. (i + 1)) `2 = (f /. (i + 2)) `2 ) by A2, A3; :: thesis: verum