let f be non constant standard special_circular_sequence; :: thesis: len f > 4
assume A1: len f <= 4 ; :: thesis: contradiction
consider i1 being Element of NAT such that
A2: i1 in dom f and
A3: (f /. i1) `1 <> (f /. 1) `1 by Th32;
consider i2 being Element of NAT such that
A4: i2 in dom f and
A5: (f /. i2) `2 <> (f /. 1) `2 by Th33;
A6: len f > 1 by Lm2;
then A7: len f >= 1 + 1 by NAT_1:13;
then A8: ( 1 in dom f & 2 in dom f ) by A6, FINSEQ_3:27;

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

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

A10: i1 <= len f by A2, FINSEQ_3:27;
A11: i1 <> 0 by A2, FINSEQ_3:27;
A12: f /. (len f) = f /. 1 by FINSEQ_6:def 1;

now

per cases ( i1 = 3 or i1 = 4 ) by A1, A3, A9, A10, A11, NAT_1:29, XXREAL_0:2;

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

then A14: len f >= 3 by A2, FINSEQ_3:27;
then len f > 3 by A3, A12, A13, XXREAL_0:1;
then A15: len f >= 3 + 1 by NAT_1:13;
then A16: len f = 4 by A1, XXREAL_0:1;

A17: now

assume (f /. (1 + 1)) `2 = (f /. 1) `2 ; :: thesis: contradiction
then f /. (1 + 1) = |[((f /. 1) `1 ),((f /. 1) `2 )]| by A9, EUCLID:57
.= f /. 1 by EUCLID:57 ;
hence contradiction by A8, Th31; :: thesis: verum

end;

A18: (f /. 2) `2 = (f /. (2 + 1)) `2 by A3, A9, A13, A14, TOPREAL1:def 7;
( (f /. 3) `1 = (f /. (3 + 1)) `1 or (f /. 3) `2 = (f /. (3 + 1)) `2 ) by A15, TOPREAL1:def 7;
hence contradiction by A3, A13, A16, A17, A18, FINSEQ_6:def 1; :: thesis: verum

end;

suppose i1 = 4 ; :: thesis: contradiction

hence contradiction by A1, A3, A10, A12, XXREAL_0:1; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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

A20: i2 <= len f by A4, FINSEQ_3:27;
A21: i2 <> 0 by A4, FINSEQ_3:27;
A22: f /. (len f) = f /. 1 by FINSEQ_6:def 1;

now

per cases ( i2 = 3 or i2 = 4 ) by A1, A5, A19, A20, A21, NAT_1:29, XXREAL_0:2;

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

then A24: len f >= 3 by A4, FINSEQ_3:27;
then len f > 3 by A5, A22, A23, XXREAL_0:1;
then A25: len f >= 3 + 1 by NAT_1:13;
then A26: len f = 4 by A1, XXREAL_0:1;

A27: now

assume (f /. (1 + 1)) `1 = (f /. 1) `1 ; :: thesis: contradiction
then f /. (1 + 1) = |[((f /. 1) `1 ),((f /. 1) `2 )]| by A19, EUCLID:57
.= f /. 1 by EUCLID:57 ;
hence contradiction by A8, Th31; :: thesis: verum

end;

A28: (f /. 2) `1 = (f /. (2 + 1)) `1 by A5, A19, A23, A24, TOPREAL1:def 7;
( (f /. 3) `2 = (f /. (3 + 1)) `2 or (f /. 3) `1 = (f /. (3 + 1)) `1 ) by A25, TOPREAL1:def 7;
hence contradiction by A5, A23, A26, A27, A28, FINSEQ_6:def 1; :: thesis: verum

end;

suppose i2 = 4 ; :: thesis: contradiction

hence contradiction by A1, A5, A20, A22, XXREAL_0:1; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;