let n be Nat; 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 ; 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; ( 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
; ( 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
; ( 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
; ( not f .: X c= NAT \ {0} or Sgm (f .: X) = f * (Sgm X) )
assume A5:
f .: X c= NAT \ {0}
; Sgm (f .: X) = f * (Sgm X)
per cases
( X misses dom f or X meets dom f )
;
suppose A8:
X meets dom f
;
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;
then A12:
f .: X c= Seg k
;
A13:
now for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len fs & k1 = fs . l & k2 = fs . m holds
k1 < k2A14:
dom fs = Seg (len fs)
by FINSEQ_1:def 3;
let l,
m,
k1,
k2 be
Nat;
( 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
;
( 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
;
k1 < k2A27:
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;
verum end;
rng fs = f .: X
by A2, RELAT_1:127;
hence
Sgm (f .: X) = f * (Sgm X)
by A12, A13, FINSEQ_1:def 13;
verum end; end;