let f be FinSequence of REAL ; :: thesis: for A being finite Subset of REAL st A = rng f holds
SgmX RealOrd ,A = Incr f
let A be finite Subset of REAL ; :: thesis: ( A = rng f implies SgmX RealOrd ,A = Incr f )
assume A1: A = rng f ; :: thesis: SgmX RealOrd ,A = Incr f
reconsider F = SgmX RealOrd ,A as increasing FinSequence of REAL by Th12;
RealOrd linearly_orders A by Th11, ORDERS_1:134;
then A2: rng (SgmX RealOrd ,A) = rng f by A1, PRE_POLY:def 2;
len F = card (rng f) by A1, Th11, ORDERS_1:134, PRE_POLY:11;
hence SgmX RealOrd ,A = Incr f by A2, GOBOARD2:def 2; :: thesis: verum