set f = <*> the carrier of (TOP-REAL 2);
let i be Nat; :: according to TOPREAL1:def 7 :: thesis: ( not 1 <= i or not i + 1 <= len (<*> the carrier of (TOP-REAL 2)) or ((<*> the carrier of (TOP-REAL 2)) /. i) `1 = ((<*> the carrier of (TOP-REAL 2)) /. (i + 1)) `1 or ((<*> the carrier of (TOP-REAL 2)) /. i) `2 = ((<*> the carrier of (TOP-REAL 2)) /. (i + 1)) `2 )
assume that
1 <= i and
A1: i + 1 <= len (<*> the carrier of (TOP-REAL 2)) ; :: thesis: ( ((<*> the carrier of (TOP-REAL 2)) /. i) `1 = ((<*> the carrier of (TOP-REAL 2)) /. (i + 1)) `1 or ((<*> the carrier of (TOP-REAL 2)) /. i) `2 = ((<*> the carrier of (TOP-REAL 2)) /. (i + 1)) `2 )
thus ( ((<*> the carrier of (TOP-REAL 2)) /. i) `1 = ((<*> the carrier of (TOP-REAL 2)) /. (i + 1)) `1 or ((<*> the carrier of (TOP-REAL 2)) /. i) `2 = ((<*> the carrier of (TOP-REAL 2)) /. (i + 1)) `2 ) by A1; :: thesis: verum