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;
per cases ( (f /. (1 + 1)) `1 = (f /. 1) `1 or (f /. (1 + 1)) `2 = (f /. 1) `2 ) by A4, TOPREAL1:def 5;
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;
now :: thesis: contradiction
i1 <= 4 by A1, A11, XXREAL_0:2;
then not not i1 = 0 & ... & not i1 = 4 ;
per cases then ( i1 = 3 or i1 = 4 ) by A9, A10, A13;
suppose A14: i1 = 3 ; :: thesis: contradiction
A15: now :: thesis: not (f /. (1 + 1)) `2 = (f /. 1) `2
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;
A16: len f >= 3 by A8, A14, FINSEQ_3:25;
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;
end;
end;
hence contradiction ; :: thesis: verum
end;
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;
now :: thesis: contradiction
i2 <= 4 by A1, A21, XXREAL_0:2;
then not not i2 = 0 & ... & not i2 = 4 ;
per cases then ( i2 = 3 or i2 = 4 ) by A7, A20, A23;
suppose A24: i2 = 3 ; :: thesis: contradiction
A25: now :: thesis: not (f /. (1 + 1)) `1 = (f /. 1) `1
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;
A26: len f >= 3 by A6, A24, FINSEQ_3:25;
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;
end;
end;
hence contradiction ; :: thesis: verum
end;
end;