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) )

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 \ {0} or Sgm (f .: X) = f * (Sgm X) )

assume A4: f | X is increasing ; :: thesis: ( not f .: X c= NAT \ {0} or Sgm (f .: X) = f * (Sgm X) )

assume A5: f .: X c= NAT \ {0} ; :: thesis: Sgm (f .: X) = f * (Sgm X)

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) )

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 \ {0} or Sgm (f .: X) = f * (Sgm X) )

assume A4: f | X is increasing ; :: thesis: ( not f .: X c= NAT \ {0} or Sgm (f .: X) = f * (Sgm X) )

assume A5: f .: X c= NAT \ {0} ; :: thesis: Sgm (f .: X) = f * (Sgm X)

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

end;

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 A7, FINSEQ_1:51;

hence Sgm (f .: X) = f * (Sgm X) by A2, A6, RELAT_1:44; :: thesis: verum

end;then f .: X c= Seg 0 ;

then Sgm (f .: X) = {} by A7, FINSEQ_1:51;

hence Sgm (f .: X) = f * (Sgm X) by A2, A6, RELAT_1:44; :: thesis: verum

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 \ {0} by A5;

then reconsider fX = f .: X as non empty finite natural-membered set by A8, AA, RELAT_1:118;

reconsider k = max fX as Nat by TARSKI:1;

set fs = f * (Sgm X);

rng (Sgm X) c= dom f by A1, A3, FINSEQ_1:def 13;

then reconsider fs = f * (Sgm X) as FinSequence by FINSEQ_1:16;

f .: (rng (Sgm X)) c= NAT \ {0} by A1, A5, FINSEQ_1:def 13;

then A9: rng fs c= NAT \ {0} by RELAT_1:127;

rng fs c= NAT by A9, XBOOLE_1:1;

then reconsider fs = fs as FinSequence of NAT by FINSEQ_1:def 4;

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

end;set fX = f .: X;

reconsider f9 = f as Function ;

AA: f9 .: X9 is finite ;

f .: X c= NAT \ {0} by A5;

then reconsider fX = f .: X as non empty finite natural-membered set by A8, AA, RELAT_1:118;

reconsider k = max fX as Nat by TARSKI:1;

set fs = f * (Sgm X);

rng (Sgm X) c= dom f by A1, A3, FINSEQ_1:def 13;

then reconsider fs = f * (Sgm X) as FinSequence by FINSEQ_1:16;

f .: (rng (Sgm X)) c= NAT \ {0} by A1, A5, FINSEQ_1:def 13;

then A9: rng fs c= NAT \ {0} by RELAT_1:127;

rng fs c= NAT by A9, XBOOLE_1:1;

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

then A12:
f .: X c= Seg k
;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 {0} by A5, A10, XBOOLE_0:def 5;

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 A10, XXREAL_2:def 8;

hence x in Seg k by A11; :: thesis: verum

end;assume A10: x in f .: X ; :: thesis: x in Seg k

then reconsider k9 = x as Nat by A5;

not k9 in {0} by A5, A10, XBOOLE_0:def 5;

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 A10, XXREAL_2:def 8;

hence x in Seg k by A11; :: thesis: verum

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

rng fs = f .: X
by A2, RELAT_1:127;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 A16, A17, XXREAL_0:2;

then A18: l in dom fs by A15, A14;

then l in dom (Sgm X) by FUNCT_1:11;

then A19: (Sgm X) . l in X by A2, FUNCT_1:3;

set k29 = (Sgm X) . m;

1 <= m by A15, A16, XXREAL_0:2;

then A20: m in dom fs by A17, A14;

then A21: m in dom (Sgm X) by FUNCT_1:11;

then A22: (Sgm X) . m in X by A2, FUNCT_1:3;

reconsider k19 = (Sgm X) . l, k29 = (Sgm X) . m as Nat ;

m in Seg (len (Sgm X)) by A21, FINSEQ_1:def 3;

then m <= len (Sgm X) by FINSEQ_1:1;

then A23: k19 < k29 by A1, A15, A16, FINSEQ_1:def 13;

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 A18, FUNCT_1:11;

then A24: k19 in X /\ (dom f) by A19, XBOOLE_0:def 4;

assume that

A25: k1 = fs . l and

A26: k2 = fs . m ; :: thesis: k1 < k2

A27: k2 = f . ((Sgm X) . m) by A26, A20, FUNCT_1:12;

(Sgm X) . m in dom f by A20, FUNCT_1:11;

then A28: k29 in X /\ (dom f) by A22, XBOOLE_0:def 4;

k1 = f . ((Sgm X) . l) by A25, A18, FUNCT_1:12;

hence k1 < k2 by A4, A27, A23, A24, A28, RFUNCT_2:20; :: thesis: verum

end;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 A16, A17, XXREAL_0:2;

then A18: l in dom fs by A15, A14;

then l in dom (Sgm X) by FUNCT_1:11;

then A19: (Sgm X) . l in X by A2, FUNCT_1:3;

set k29 = (Sgm X) . m;

1 <= m by A15, A16, XXREAL_0:2;

then A20: m in dom fs by A17, A14;

then A21: m in dom (Sgm X) by FUNCT_1:11;

then A22: (Sgm X) . m in X by A2, FUNCT_1:3;

reconsider k19 = (Sgm X) . l, k29 = (Sgm X) . m as Nat ;

m in Seg (len (Sgm X)) by A21, FINSEQ_1:def 3;

then m <= len (Sgm X) by FINSEQ_1:1;

then A23: k19 < k29 by A1, A15, A16, FINSEQ_1:def 13;

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 A18, FUNCT_1:11;

then A24: k19 in X /\ (dom f) by A19, XBOOLE_0:def 4;

assume that

A25: k1 = fs . l and

A26: k2 = fs . m ; :: thesis: k1 < k2

A27: k2 = f . ((Sgm X) . m) by A26, A20, FUNCT_1:12;

(Sgm X) . m in dom f by A20, FUNCT_1:11;

then A28: k29 in X /\ (dom f) by A22, XBOOLE_0:def 4;

k1 = f . ((Sgm X) . l) by A25, A18, FUNCT_1:12;

hence k1 < k2 by A4, A27, A23, A24, A28, RFUNCT_2:20; :: thesis: verum

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