set f = Sgm X;
let a be Nat; :: according to EUCLID_7:def 1 :: thesis: ( not 1 <= a or len (Sgm X) <= a or not (Sgm X) . (a + 1) <= (Sgm X) . a )
assume that
A1: 1 <= a and
A2: a < len (Sgm X) ; :: thesis: not (Sgm X) . (a + 1) <= (Sgm X) . a
A3: a + 0 < a + 1 by XREAL_1:8;
a + 1 <= len (Sgm X) by A2, NAT_1:13;
hence (Sgm X) . a < (Sgm X) . (a + 1) by A1, A3, FINSEQ_1:def 14; :: thesis: verum