let n be Nat; :: thesis: for X being set
for f being PartFunc of REAL ,REAL st X c= Seg n & X c= dom f & f | X is increasing & f .: X c= NAT \ {0 } holds
Sgm (f .: X) = f * (Sgm X)
let X be set ; :: thesis: for f being PartFunc of REAL ,REAL st X c= Seg n & X c= dom f & f | X is increasing & f .: X c= NAT \ {0 } holds
Sgm (f .: X) = f * (Sgm X)
let f be PartFunc of REAL ,REAL ; :: thesis: ( X c= Seg n & X c= dom f & f | X is increasing & f .: X c= NAT \ {0 } implies Sgm (f .: X) = f * (Sgm X) )
assume A1: X c= Seg n ; :: thesis: ( not X c= dom f or not f | X is increasing or not f .: X c= NAT \ {0 } or Sgm (f .: X) = f * (Sgm X) )
assume A2: X c= dom f ; :: thesis: ( not f | X is increasing or not f .: X c= NAT \ {0 } or Sgm (f .: X) = f * (Sgm X) )
assume A3: f | X is increasing ; :: thesis: ( not f .: X c= NAT \ {0 } or Sgm (f .: X) = f * (Sgm X) )
assume A4: f .: X c= NAT \ {0 } ; :: thesis: Sgm (f .: X) = f * (Sgm X)
A5: rng (Sgm X) = X by A1, FINSEQ_1:def 13;

per cases ( X misses dom f or X meets dom f ) ;

suppose A6: X misses dom f ; :: thesis: Sgm (f .: X) = f * (Sgm X)

then f .: X = {} by RELAT_1:151;
then Sgm (f .: X) = {} by FINSEQ_1:4, FINSEQ_1:72;
hence Sgm (f .: X) = f * (Sgm X) by A5, A6, RELAT_1:67; :: thesis: verum

end;

suppose A7: X meets dom f ; :: thesis: Sgm (f .: X) = f * (Sgm X)

set fs = f * (Sgm X);
set fX = f .: X;
rng (Sgm X) c= dom f by A1, A2, FINSEQ_1:def 13;
then reconsider fs = f * (Sgm X) as FinSequence by FINSEQ_1:20;
f .: (rng (Sgm X)) c= NAT \ {0 } by A1, A4, FINSEQ_1:def 13;
then A8: rng fs c= NAT \ {0 } by RELAT_1:160;
NAT \ {0 } c= NAT by XBOOLE_1:36;
then rng fs c= NAT by A8, XBOOLE_1:1;
then reconsider fs = fs as FinSequence of NAT by FINSEQ_1:def 4;
reconsider f' = f as Function ;
reconsider X' = X as finite set by A1;
f' .: X' is finite ;
then reconsider fX = f .: X as non empty finite real-membered set by A7, RELAT_1:151;
set k = max fX;
max fX in fX by XXREAL_2:def 8;
then max fX in NAT \ {0 } by A4;
then reconsider k = max fX as Nat ;

now

let x be set ; :: thesis: ( x in f .: X implies x in Seg k )
assume A10: x in f .: X ; :: thesis: x in Seg k
then x in NAT \ {0 } by A4;
then reconsider k' = x as Nat ;
A11: k' <= k by A10, XXREAL_2:def 8;
not k' in {0 } by A4, A10, XBOOLE_0:def 5;
then k' <> 0 by TARSKI:def 1;
then 0 < k' ;
then 0 + 1 < k' + 1 by XREAL_1:8;
then 1 <= k' by NAT_1:13;
hence x in Seg k by A11, FINSEQ_1:3; :: thesis: verum

end;

then A12: f .: X c= Seg k by TARSKI:def 3;
A13: rng fs = f .: X by A5, RELAT_1:160;

now

let l, m, k1, k2 be Nat; :: thesis: ( 1 <= l & l < m & m <= len fs & k1 = fs . l & k2 = fs . m implies k1 < k2 )
assume A14: ( 1 <= l & l < m & m <= len fs ) ; :: thesis: ( k1 = fs . l & k2 = fs . m implies k1 < k2 )
assume A15: ( k1 = fs . l & k2 = fs . m ) ; :: thesis: k1 < k2
A16: dom fs = Seg (len fs) by FINSEQ_1:def 3;
( 1 <= l & l <= len fs ) by A14, XXREAL_0:2;
then A17: l in dom fs by A16, FINSEQ_1:3;
then A18: ( l in dom (Sgm X) & (Sgm X) . l in dom f ) by FUNCT_1:21;
( 1 <= m & m <= len fs ) by A14, XXREAL_0:2;
then A19: m in dom fs by A16, FINSEQ_1:3;
then A20: ( m in dom (Sgm X) & (Sgm X) . m in dom f ) by FUNCT_1:21;
A21: ( k1 = f . ((Sgm X) . l) & k2 = f . ((Sgm X) . m) ) by A15, A17, A19, FUNCT_1:22;
set k1' = (Sgm X) . l;
set k2' = (Sgm X) . m;
A22: ( (Sgm X) . l in X & (Sgm X) . m in X ) by A5, A18, A20, FUNCT_1:12;
reconsider k1' = (Sgm X) . l, k2' = (Sgm X) . m as Nat ;
m in Seg (len (Sgm X)) by A20, FINSEQ_1:def 3;
then ( 1 <= l & l < m & m <= len (Sgm X) ) by A14, FINSEQ_1:3;
then A23: k1' < k2' by A1, FINSEQ_1:def 13;
reconsider k1' = k1', k2' = k2' as Element of NAT by ORDINAL1:def 13;
reconsider k1' = k1', k2' = k2' as Element of REAL ;
( k1' in X /\ (dom f) & k2' in X /\ (dom f) ) by A18, A20, A22, XBOOLE_0:def 4;
hence k1 < k2 by A3, A21, A23, RFUNCT_2:43; :: thesis: verum

end;

hence Sgm (f .: X) = f * (Sgm X) by A12, A13, FINSEQ_1:def 13; :: thesis: verum

end;

end;