let i be Nat; :: according to TOPREAL1:def 5 :: thesis: ( not 1 <= i or not i + 1 <= len <*p*> or (<*p*> /. i) `1 = (<*p*> /. (i + 1)) `1 or (<*p*> /. i) `2 = (<*p*> /. (i + 1)) `2 )
assume that
A1: 1 <= i and
A2: i + 1 <= len <*p*> ; :: thesis: ( (<*p*> /. i) `1 = (<*p*> /. (i + 1)) `1 or (<*p*> /. i) `2 = (<*p*> /. (i + 1)) `2 )
len <*p*> = 0 + 1 by FINSEQ_1:39;
hence ( (<*p*> /. i) `1 = (<*p*> /. (i + 1)) `1 or (<*p*> /. i) `2 = (<*p*> /. (i + 1)) `2 ) by A1, A2, XREAL_1:6; :: thesis: verum