let f be non constant standard special_circular_sequence; :: thesis: ( f /. 1 = N-max (L~ f) & N-max (L~ f) <> E-max (L~ f) implies (N-max (L~ f)) .. f < (E-max (L~ f)) .. f )
A1: E-max (L~ f) in rng f by SPRECT_2:50;
A2: N-max (L~ f) in rng f by SPRECT_2:44;
assume that
A3: f /. 1 = N-max (L~ f) and
A4: N-max (L~ f) <> E-max (L~ f) ; :: thesis: (N-max (L~ f)) .. f < (E-max (L~ f)) .. f
A5: (N-max (L~ f)) .. f = 1 by A3, FINSEQ_6:47;
(E-max (L~ f)) .. f in dom f by A1, FINSEQ_4:30;
then (E-max (L~ f)) .. f >= 1 by FINSEQ_3:27;
hence (N-max (L~ f)) .. f < (E-max (L~ f)) .. f by A1, A2, A4, A5, FINSEQ_5:10, XXREAL_0:1; :: thesis: verum