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 \ 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 \ 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 \ 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 \ or Sgm (f .: X) = f * (Sgm X) )
then A2: rng (Sgm X) = X by FINSEQ_1:def 13;
assume A3: X c= dom f ; :: thesis: ( not f | X is increasing or not f .: X c= NAT \ or Sgm (f .: X) = f * (Sgm X) )
assume A4: f | X is increasing ; :: thesis: ( not f .: X c= NAT \ or Sgm (f .: X) = f * (Sgm X) )
assume A5: f .: X c= NAT \ ; :: thesis: Sgm (f .: X) = f * (Sgm X)
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 A7: f .: X = {} by RELAT_1:118;
then f .: X c= Seg 0 ;
then Sgm (f .: X) = {} by ;
hence Sgm (f .: X) = f * (Sgm X) by ; :: thesis: verum
end;
suppose A8: X meets dom f ; :: thesis: Sgm (f .: X) = f * (Sgm X)
reconsider X9 = X as finite set by A1;
set fX = f .: X;
reconsider f9 = f as Function ;
AA: f9 .: X9 is finite ;
f .: X c= NAT \ by A5;
then reconsider fX = f .: X as non empty finite natural-membered set by ;
reconsider k = max fX as Nat by TARSKI:1;
set fs = f * (Sgm X);
rng (Sgm X) c= dom f by ;
then reconsider fs = f * (Sgm X) as FinSequence by FINSEQ_1:16;
f .: (rng (Sgm X)) c= NAT \ by ;
then A9: rng fs c= NAT \ by RELAT_1:127;
rng fs c= NAT by ;
then reconsider fs = fs as FinSequence of NAT by FINSEQ_1:def 4;
now :: thesis: for x being object st x in f .: X holds
x in Seg k
let x be object ; :: thesis: ( x in f .: X implies x in Seg k )
assume A10: x in f .: X ; :: thesis: x in Seg k
then reconsider k9 = x as Nat by A5;
not k9 in by ;
then k9 <> 0 by TARSKI:def 1;
then 0 + 1 < k9 + 1 by XREAL_1:6;
then A11: 1 <= k9 by NAT_1:13;
k9 <= k by ;
hence x in Seg k by A11; :: thesis: verum
end;
then A12: f .: X c= Seg k ;
A13: now :: thesis: for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len fs & k1 = fs . l & k2 = fs . m holds
k1 < k2
A14: dom fs = Seg (len fs) by FINSEQ_1:def 3;
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 that
A15: 1 <= l and
A16: l < m and
A17: m <= len fs ; :: thesis: ( k1 = fs . l & k2 = fs . m implies k1 < k2 )
set k19 = (Sgm X) . l;
l <= len fs by ;
then A18: l in dom fs by ;
then l in dom (Sgm X) by FUNCT_1:11;
then A19: (Sgm X) . l in X by ;
set k29 = (Sgm X) . m;
1 <= m by ;
then A20: m in dom fs by ;
then A21: m in dom (Sgm X) by FUNCT_1:11;
then A22: (Sgm X) . m in X by ;
reconsider k19 = (Sgm X) . l, k29 = (Sgm X) . m as Nat ;
m in Seg (len (Sgm X)) by ;
then m <= len (Sgm X) by FINSEQ_1:1;
then A23: k19 < k29 by ;
reconsider k19 = k19, k29 = k29 as Element of NAT by ORDINAL1:def 12;
reconsider k19 = k19, k29 = k29 as Element of REAL by XREAL_0:def 1;
(Sgm X) . l in dom f by ;
then A24: k19 in X /\ (dom f) by ;
assume that
A25: k1 = fs . l and
A26: k2 = fs . m ; :: thesis: k1 < k2
A27: k2 = f . ((Sgm X) . m) by ;
(Sgm X) . m in dom f by ;
then A28: k29 in X /\ (dom f) by ;
k1 = f . ((Sgm X) . l) by ;
hence k1 < k2 by ; :: thesis: verum
end;
rng fs = f .: X by ;
hence Sgm (f .: X) = f * (Sgm X) by ; :: thesis: verum
end;
end;