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 ;
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 ;
suppose A10: (f /. (1 + 1)) `1 = (f /. 1) `1 ; :: thesis: contradiction
A11: i1 <= len f by ;
A12: f /. (len f) = f /. 1 by FINSEQ_6:def 1;
A13: i1 <> 0 by ;
i1 <= 4 by ;
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
.= f /. 1 by EUCLID:53 ;
hence contradiction by A3, A5, Th29; :: thesis: verum
end;
A16: len f >= 3 by ;
then len f > 3 by ;
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 ;
(f /. 2) `2 = (f /. (2 + 1)) `2 by ;
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 ;
A22: f /. (len f) = f /. 1 by FINSEQ_6:def 1;
A23: i2 <> 0 by ;
i2 <= 4 by ;
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
.= f /. 1 by EUCLID:53 ;
hence contradiction by A3, A5, Th29; :: thesis: verum
end;
A26: len f >= 3 by ;
then len f > 3 by ;
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 ;
(f /. 2) `1 = (f /. (2 + 1)) `1 by ;
hence contradiction by A7, A24, A29, A25, A28, FINSEQ_6:def 1; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
end;