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 Th7;
RealOrd linearly_orders A by Th6, ORDERS_1:38;
then A2: rng (SgmX (RealOrd,A)) = rng f by A1, PRE_POLY:def 2;
len F = card (rng f) by A1, Th6, ORDERS_1:38, PRE_POLY:11;
hence SgmX (RealOrd,A) = Incr f by A2, SEQ_4:def 21; :: thesis: verum