let f be V8() standard special_circular_sequence; :: thesis: len f > 4

assume A1: len f <= 4 ; :: thesis: contradiction

A2: len f > 1 by Lm2;

then A3: 1 in dom f by FINSEQ_3:25;

A4: len f >= 1 + 1 by A2, NAT_1:13;

then A5: 2 in dom f by FINSEQ_3:25;

consider i2 being Nat such that

A6: i2 in dom f and

A7: (f /. i2) `2 <> (f /. 1) `2 by Th31;

consider i1 being Nat such that

A8: i1 in dom f and

A9: (f /. i1) `1 <> (f /. 1) `1 by Th30;

assume A1: len f <= 4 ; :: thesis: contradiction

A2: len f > 1 by Lm2;

then A3: 1 in dom f by FINSEQ_3:25;

A4: len f >= 1 + 1 by A2, NAT_1:13;

then A5: 2 in dom f by FINSEQ_3:25;

consider i2 being Nat such that

A6: i2 in dom f and

A7: (f /. i2) `2 <> (f /. 1) `2 by Th31;

consider i1 being Nat such that

A8: i1 in dom f and

A9: (f /. i1) `1 <> (f /. 1) `1 by Th30;

per cases
( (f /. (1 + 1)) `1 = (f /. 1) `1 or (f /. (1 + 1)) `2 = (f /. 1) `2 )
by A4, TOPREAL1:def 5;

end;

suppose A10:
(f /. (1 + 1)) `1 = (f /. 1) `1
; :: thesis: contradiction

A11:
i1 <= len f
by A8, FINSEQ_3:25;

A12: f /. (len f) = f /. 1 by FINSEQ_6:def 1;

A13: i1 <> 0 by A8, FINSEQ_3:25;

end;A12: f /. (len f) = f /. 1 by FINSEQ_6:def 1;

A13: i1 <> 0 by A8, FINSEQ_3:25;

now :: thesis: contradiction

hence
contradiction
; :: thesis: verum
i1 <= 4
by A1, A11, XXREAL_0:2;

then not not i1 = 0 & ... & not i1 = 4 ;

end;then not not i1 = 0 & ... & not i1 = 4 ;

per cases then
( i1 = 3 or i1 = 4 )
by A9, A10, A13;

end;

suppose A14:
i1 = 3
; :: thesis: contradiction

then len f > 3 by A9, A12, A14, XXREAL_0:1;

then A17: len f >= 3 + 1 by NAT_1:13;

then A18: ( (f /. 3) `1 = (f /. (3 + 1)) `1 or (f /. 3) `2 = (f /. (3 + 1)) `2 ) by TOPREAL1:def 5;

A19: len f = 4 by A1, A17, XXREAL_0:1;

(f /. 2) `2 = (f /. (2 + 1)) `2 by A9, A10, A14, A16, TOPREAL1:def 5;

hence contradiction by A9, A14, A19, A15, A18, FINSEQ_6:def 1; :: thesis: verum

end;

A15: now :: thesis: not (f /. (1 + 1)) `2 = (f /. 1) `2

A16:
len f >= 3
by A8, A14, FINSEQ_3:25;assume
(f /. (1 + 1)) `2 = (f /. 1) `2
; :: thesis: contradiction

then f /. (1 + 1) = |[((f /. 1) `1),((f /. 1) `2)]| by A10, EUCLID:53

.= f /. 1 by EUCLID:53 ;

hence contradiction by A3, A5, Th29; :: thesis: verum

end;then f /. (1 + 1) = |[((f /. 1) `1),((f /. 1) `2)]| by A10, EUCLID:53

.= f /. 1 by EUCLID:53 ;

hence contradiction by A3, A5, Th29; :: thesis: verum

then len f > 3 by A9, A12, A14, XXREAL_0:1;

then A17: len f >= 3 + 1 by NAT_1:13;

then A18: ( (f /. 3) `1 = (f /. (3 + 1)) `1 or (f /. 3) `2 = (f /. (3 + 1)) `2 ) by TOPREAL1:def 5;

A19: len f = 4 by A1, A17, XXREAL_0:1;

(f /. 2) `2 = (f /. (2 + 1)) `2 by A9, A10, A14, A16, TOPREAL1:def 5;

hence contradiction by A9, A14, A19, A15, A18, FINSEQ_6:def 1; :: thesis: verum

suppose A20:
(f /. (1 + 1)) `2 = (f /. 1) `2
; :: thesis: contradiction

A21:
i2 <= len f
by A6, FINSEQ_3:25;

A22: f /. (len f) = f /. 1 by FINSEQ_6:def 1;

A23: i2 <> 0 by A6, FINSEQ_3:25;

end;A22: f /. (len f) = f /. 1 by FINSEQ_6:def 1;

A23: i2 <> 0 by A6, FINSEQ_3:25;

now :: thesis: contradiction

hence
contradiction
; :: thesis: verum
i2 <= 4
by A1, A21, XXREAL_0:2;

then not not i2 = 0 & ... & not i2 = 4 ;

end;then not not i2 = 0 & ... & not i2 = 4 ;

per cases then
( i2 = 3 or i2 = 4 )
by A7, A20, A23;

end;

suppose A24:
i2 = 3
; :: thesis: contradiction

then len f > 3 by A7, A22, A24, XXREAL_0:1;

then A27: len f >= 3 + 1 by NAT_1:13;

then A28: ( (f /. 3) `2 = (f /. (3 + 1)) `2 or (f /. 3) `1 = (f /. (3 + 1)) `1 ) by TOPREAL1:def 5;

A29: len f = 4 by A1, A27, XXREAL_0:1;

(f /. 2) `1 = (f /. (2 + 1)) `1 by A7, A20, A24, A26, TOPREAL1:def 5;

hence contradiction by A7, A24, A29, A25, A28, FINSEQ_6:def 1; :: thesis: verum

end;

A25: now :: thesis: not (f /. (1 + 1)) `1 = (f /. 1) `1

A26:
len f >= 3
by A6, A24, FINSEQ_3:25;assume
(f /. (1 + 1)) `1 = (f /. 1) `1
; :: thesis: contradiction

then f /. (1 + 1) = |[((f /. 1) `1),((f /. 1) `2)]| by A20, EUCLID:53

.= f /. 1 by EUCLID:53 ;

hence contradiction by A3, A5, Th29; :: thesis: verum

end;then f /. (1 + 1) = |[((f /. 1) `1),((f /. 1) `2)]| by A20, EUCLID:53

.= f /. 1 by EUCLID:53 ;

hence contradiction by A3, A5, Th29; :: thesis: verum

then len f > 3 by A7, A22, A24, XXREAL_0:1;

then A27: len f >= 3 + 1 by NAT_1:13;

then A28: ( (f /. 3) `2 = (f /. (3 + 1)) `2 or (f /. 3) `1 = (f /. (3 + 1)) `1 ) by TOPREAL1:def 5;

A29: len f = 4 by A1, A27, XXREAL_0:1;

(f /. 2) `1 = (f /. (2 + 1)) `1 by A7, A20, A24, A26, TOPREAL1:def 5;

hence contradiction by A7, A24, A29, A25, A28, FINSEQ_6:def 1; :: thesis: verum