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
RealOrd linearly_orders A by Th11, ORDERS_1:134;
then A2: rng (SgmX RealOrd ,A) = rng f by A1, TRIANG_1:def 2;
reconsider F = SgmX RealOrd ,A as increasing FinSequence of REAL by Th12;
len F = card (rng f) by A1, Th11, ORDERS_1:134, TRIANG_1:9;
hence SgmX RealOrd ,A = Incr f by A2, GOBOARD2:def 2; :: thesis: verum