:: RFINSEQ semantic presentation
begin
registration
let f be FinSequence;
let x be set ;
cluster Coim (f,x) -> finite ;
coherence
Coim (f,x) is finite ;
end;
theorem Th1: :: RFINSEQ:1
for f, g, h being FinSequence holds
( f,g are_fiberwise_equipotent iff f ^ h,g ^ h are_fiberwise_equipotent )
proof
let f, g, h be FinSequence; ::_thesis: ( f,g are_fiberwise_equipotent iff f ^ h,g ^ h are_fiberwise_equipotent )
thus ( f,g are_fiberwise_equipotent implies f ^ h,g ^ h are_fiberwise_equipotent ) ::_thesis: ( f ^ h,g ^ h are_fiberwise_equipotent implies f,g are_fiberwise_equipotent )
proof
assume A1: f,g are_fiberwise_equipotent ; ::_thesis: f ^ h,g ^ h are_fiberwise_equipotent
now__::_thesis:_for_y_being_set_holds_card_(Coim_((f_^_h),y))_=_card_(Coim_((g_^_h),y))
let y be set ; ::_thesis: card (Coim ((f ^ h),y)) = card (Coim ((g ^ h),y))
card (Coim (f,y)) = card (Coim (g,y)) by A1, CLASSES1:def_9;
hence card (Coim ((f ^ h),y)) = (card (Coim (g,y))) + (card (Coim (h,y))) by FINSEQ_3:57
.= card (Coim ((g ^ h),y)) by FINSEQ_3:57 ;
::_thesis: verum
end;
hence f ^ h,g ^ h are_fiberwise_equipotent by CLASSES1:def_9; ::_thesis: verum
end;
assume A2: f ^ h,g ^ h are_fiberwise_equipotent ; ::_thesis: f,g are_fiberwise_equipotent
now__::_thesis:_for_x_being_set_holds_card_(Coim_(f,x))_=_card_(Coim_(g,x))
let x be set ; ::_thesis: card (Coim (f,x)) = card (Coim (g,x))
A3: ( card (Coim ((f ^ h),x)) = (card (Coim (f,x))) + (card (Coim (h,x))) & card (Coim ((g ^ h),x)) = (card (Coim (g,x))) + (card (Coim (h,x))) ) by FINSEQ_3:57;
card (Coim ((f ^ h),x)) = card (Coim ((g ^ h),x)) by A2, CLASSES1:def_9;
hence card (Coim (f,x)) = card (Coim (g,x)) by A3; ::_thesis: verum
end;
hence f,g are_fiberwise_equipotent by CLASSES1:def_9; ::_thesis: verum
end;
theorem :: RFINSEQ:2
for f, g being FinSequence holds f ^ g,g ^ f are_fiberwise_equipotent
proof
let f, g be FinSequence; ::_thesis: f ^ g,g ^ f are_fiberwise_equipotent
let y be set ; :: according to CLASSES1:def_9 ::_thesis: card (Coim ((f ^ g),y)) = card (Coim ((g ^ f),y))
thus card (Coim ((f ^ g),y)) = (card (g " {y})) + (card (f " {y})) by FINSEQ_3:57
.= card (Coim ((g ^ f),y)) by FINSEQ_3:57 ; ::_thesis: verum
end;
theorem Th3: :: RFINSEQ:3
for f, g being FinSequence st f,g are_fiberwise_equipotent holds
( len f = len g & dom f = dom g )
proof
let f, g be FinSequence; ::_thesis: ( f,g are_fiberwise_equipotent implies ( len f = len g & dom f = dom g ) )
A1: dom f = Seg (len f) by FINSEQ_1:def_3;
assume f,g are_fiberwise_equipotent ; ::_thesis: ( len f = len g & dom f = dom g )
then A2: ( card (f " (rng f)) = card (g " (rng f)) & rng f = rng g ) by CLASSES1:75, CLASSES1:78;
A3: Seg (len g) = dom g by FINSEQ_1:def_3;
thus len f = card (Seg (len f)) by FINSEQ_1:57
.= card (g " (rng g)) by A1, A2, RELAT_1:134
.= card (Seg (len g)) by A3, RELAT_1:134
.= len g by FINSEQ_1:57 ; ::_thesis: dom f = dom g
hence dom f = dom g by A1, FINSEQ_1:def_3; ::_thesis: verum
end;
theorem Th4: :: RFINSEQ:4
for f, g being FinSequence holds
( f,g are_fiberwise_equipotent iff ex P being Permutation of (dom g) st f = g * P )
proof
let f, g be FinSequence; ::_thesis: ( f,g are_fiberwise_equipotent iff ex P being Permutation of (dom g) st f = g * P )
thus ( f,g are_fiberwise_equipotent implies ex P being Permutation of (dom g) st f = g * P ) ::_thesis: ( ex P being Permutation of (dom g) st f = g * P implies f,g are_fiberwise_equipotent )
proof
assume A1: f,g are_fiberwise_equipotent ; ::_thesis: ex P being Permutation of (dom g) st f = g * P
then dom f = dom g by Th3;
hence ex P being Permutation of (dom g) st f = g * P by A1, CLASSES1:80; ::_thesis: verum
end;
given P being Permutation of (dom g) such that A2: f = g * P ; ::_thesis: f,g are_fiberwise_equipotent
( dom g = {} implies dom g = {} ) ;
then ( rng P c= dom g & dom P = dom g ) by FUNCT_2:def_1, RELAT_1:def_19;
then dom f = dom g by A2, RELAT_1:27;
hence f,g are_fiberwise_equipotent by A2, CLASSES1:80; ::_thesis: verum
end;
defpred S1[ Nat] means for X being finite set
for F being Function st card (dom (F | X)) = $1 holds
ex a being FinSequence st F | X,a are_fiberwise_equipotent ;
Lm1: S1[ 0 ]
proof
let X be finite set ; ::_thesis: for F being Function st card (dom (F | X)) = 0 holds
ex a being FinSequence st F | X,a are_fiberwise_equipotent
let F be Function; ::_thesis: ( card (dom (F | X)) = 0 implies ex a being FinSequence st F | X,a are_fiberwise_equipotent )
assume A1: card (dom (F | X)) = 0 ; ::_thesis: ex a being FinSequence st F | X,a are_fiberwise_equipotent
take A = {} ; ::_thesis: F | X,A are_fiberwise_equipotent
let x be set ; :: according to CLASSES1:def_9 ::_thesis: card (Coim ((F | X),x)) = card (Coim (A,x))
dom (F | X) = {} by A1;
hence card (Coim ((F | X),x)) = card (Coim (A,x)) by RELAT_1:132, XBOOLE_1:3; ::_thesis: verum
end;
Lm2: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A1: S1[n] ; ::_thesis: S1[n + 1]
let X be finite set ; ::_thesis: for F being Function st card (dom (F | X)) = n + 1 holds
ex a being FinSequence st F | X,a are_fiberwise_equipotent
let F be Function; ::_thesis: ( card (dom (F | X)) = n + 1 implies ex a being FinSequence st F | X,a are_fiberwise_equipotent )
reconsider dx = dom (F | X) as finite set ;
set x = the Element of dx;
set Y = X \ { the Element of dx};
set dy = dom (F | (X \ { the Element of dx}));
A2: dom (F | (X \ { the Element of dx})) = (dom F) /\ (X \ { the Element of dx}) by RELAT_1:61;
A3: dx = (dom F) /\ X by RELAT_1:61;
A4: dom (F | (X \ { the Element of dx})) = dx \ { the Element of dx}
proof
thus dom (F | (X \ { the Element of dx})) c= dx \ { the Element of dx} :: according to XBOOLE_0:def_10 ::_thesis: dx \ { the Element of dx} c= dom (F | (X \ { the Element of dx}))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in dom (F | (X \ { the Element of dx})) or y in dx \ { the Element of dx} )
assume A5: y in dom (F | (X \ { the Element of dx})) ; ::_thesis: y in dx \ { the Element of dx}
then y in X \ { the Element of dx} by A2, XBOOLE_0:def_4;
then A6: not y in { the Element of dx} by XBOOLE_0:def_5;
y in dom F by A2, A5, XBOOLE_0:def_4;
then y in dx by A2, A3, A5, XBOOLE_0:def_4;
hence y in dx \ { the Element of dx} by A6, XBOOLE_0:def_5; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in dx \ { the Element of dx} or y in dom (F | (X \ { the Element of dx})) )
assume A7: y in dx \ { the Element of dx} ; ::_thesis: y in dom (F | (X \ { the Element of dx}))
then ( not y in { the Element of dx} & y in X ) by A3, XBOOLE_0:def_4, XBOOLE_0:def_5;
then A8: y in X \ { the Element of dx} by XBOOLE_0:def_5;
y in dom F by A3, A7, XBOOLE_0:def_4;
hence y in dom (F | (X \ { the Element of dx})) by A2, A8, XBOOLE_0:def_4; ::_thesis: verum
end;
assume A9: card (dom (F | X)) = n + 1 ; ::_thesis: ex a being FinSequence st F | X,a are_fiberwise_equipotent
then { the Element of dx} c= dx by CARD_1:27, ZFMISC_1:31;
then card (dom (F | (X \ { the Element of dx}))) = (card dx) - (card { the Element of dx}) by A4, CARD_2:44
.= (n + 1) - 1 by A9, CARD_1:30
.= n ;
then consider a being FinSequence such that
A10: F | (X \ { the Element of dx}),a are_fiberwise_equipotent by A1;
take A = a ^ <*(F . the Element of dx)*>; ::_thesis: F | X,A are_fiberwise_equipotent
dx <> {} by A9;
then the Element of dx in dx ;
then A11: the Element of dx in (dom F) /\ X by RELAT_1:61;
then the Element of dx in dom F by XBOOLE_0:def_4;
then A12: { the Element of dx} c= dom F by ZFMISC_1:31;
the Element of dx in X by A11, XBOOLE_0:def_4;
then A13: { the Element of dx} c= X by ZFMISC_1:31;
now__::_thesis:_for_y_being_set_holds_card_(Coim_((F_|_X),y))_=_card_(Coim_(A,y))
let y be set ; ::_thesis: card (Coim ((F | X),y)) = card (Coim (A,y))
A14: X \ { the Element of dx} misses { the Element of dx} by XBOOLE_1:79;
A15: ((F | (X \ { the Element of dx})) " {y}) \/ ((F | { the Element of dx}) " {y}) = ((X \ { the Element of dx}) /\ (F " {y})) \/ ((F | { the Element of dx}) " {y}) by FUNCT_1:70
.= ((X \ { the Element of dx}) /\ (F " {y})) \/ ({ the Element of dx} /\ (F " {y})) by FUNCT_1:70
.= ((X \ { the Element of dx}) \/ { the Element of dx}) /\ (F " {y}) by XBOOLE_1:23
.= (X \/ { the Element of dx}) /\ (F " {y}) by XBOOLE_1:39
.= X /\ (F " {y}) by A13, XBOOLE_1:12
.= (F | X) " {y} by FUNCT_1:70 ;
reconsider FF = <*(F . the Element of dx)*> " {y} as finite set ;
A16: card (Coim ((F | (X \ { the Element of dx})),y)) = card (Coim (a,y)) by A10, CLASSES1:def_9;
A17: dom (F | { the Element of dx}) = { the Element of dx} by A12, RELAT_1:62;
A18: dom <*(F . the Element of dx)*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
A19: now__::_thesis:_(_(_y_=_F_._the_Element_of_dx_&_card_((F_|_{_the_Element_of_dx})_"_{y})_=_card_FF_)_or_(_y_<>_F_._the_Element_of_dx_&_card_((F_|_{_the_Element_of_dx})_"_{y})_=_card_FF_)_)
percases ( y = F . the Element of dx or y <> F . the Element of dx ) ;
caseA20: y = F . the Element of dx ; ::_thesis: card ((F | { the Element of dx}) " {y}) = card FF
A21: { the Element of dx} c= (F | { the Element of dx}) " {y}
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { the Element of dx} or z in (F | { the Element of dx}) " {y} )
A22: y in {y} by TARSKI:def_1;
assume A23: z in { the Element of dx} ; ::_thesis: z in (F | { the Element of dx}) " {y}
then z = the Element of dx by TARSKI:def_1;
then y = (F | { the Element of dx}) . z by A17, A20, A23, FUNCT_1:47;
hence z in (F | { the Element of dx}) " {y} by A17, A23, A22, FUNCT_1:def_7; ::_thesis: verum
end;
(F | { the Element of dx}) " {y} c= { the Element of dx} by A17, RELAT_1:132;
then (F | { the Element of dx}) " {y} = { the Element of dx} by A21, XBOOLE_0:def_10;
then A24: card ((F | { the Element of dx}) " {y}) = 1 by CARD_1:30;
A25: {1} c= <*(F . the Element of dx)*> " {y}
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {1} or z in <*(F . the Element of dx)*> " {y} )
A26: y in {y} by TARSKI:def_1;
assume A27: z in {1} ; ::_thesis: z in <*(F . the Element of dx)*> " {y}
then z = 1 by TARSKI:def_1;
then y = <*(F . the Element of dx)*> . z by A20, FINSEQ_1:40;
hence z in <*(F . the Element of dx)*> " {y} by A18, A27, A26, FUNCT_1:def_7; ::_thesis: verum
end;
<*(F . the Element of dx)*> " {y} c= {1} by A18, RELAT_1:132;
then <*(F . the Element of dx)*> " {y} = {1} by A25, XBOOLE_0:def_10;
hence card ((F | { the Element of dx}) " {y}) = card FF by A24, CARD_1:30; ::_thesis: verum
end;
caseA28: y <> F . the Element of dx ; ::_thesis: card ((F | { the Element of dx}) " {y}) = card FF
A29: now__::_thesis:_not_<*(F_._the_Element_of_dx)*>_"_{y}_<>_{}
set z = the Element of <*(F . the Element of dx)*> " {y};
assume A30: <*(F . the Element of dx)*> " {y} <> {} ; ::_thesis: contradiction
then <*(F . the Element of dx)*> . the Element of <*(F . the Element of dx)*> " {y} in {y} by FUNCT_1:def_7;
then A31: <*(F . the Element of dx)*> . the Element of <*(F . the Element of dx)*> " {y} = y by TARSKI:def_1;
the Element of <*(F . the Element of dx)*> " {y} in {1} by A18, A30, FUNCT_1:def_7;
then the Element of <*(F . the Element of dx)*> " {y} = 1 by TARSKI:def_1;
hence contradiction by A28, A31, FINSEQ_1:40; ::_thesis: verum
end;
now__::_thesis:_not_(F_|_{_the_Element_of_dx})_"_{y}_<>_{}
set z = the Element of (F | { the Element of dx}) " {y};
assume A32: (F | { the Element of dx}) " {y} <> {} ; ::_thesis: contradiction
then (F | { the Element of dx}) . the Element of (F | { the Element of dx}) " {y} in {y} by FUNCT_1:def_7;
then A33: (F | { the Element of dx}) . the Element of (F | { the Element of dx}) " {y} = y by TARSKI:def_1;
A34: the Element of (F | { the Element of dx}) " {y} in { the Element of dx} by A17, A32, FUNCT_1:def_7;
then the Element of (F | { the Element of dx}) " {y} = the Element of dx by TARSKI:def_1;
hence contradiction by A17, A28, A34, A33, FUNCT_1:47; ::_thesis: verum
end;
hence card ((F | { the Element of dx}) " {y}) = card FF by A29; ::_thesis: verum
end;
end;
end;
((F | (X \ { the Element of dx})) " {y}) /\ ((F | { the Element of dx}) " {y}) = ((X \ { the Element of dx}) /\ (F " {y})) /\ ((F | { the Element of dx}) " {y}) by FUNCT_1:70
.= ((X \ { the Element of dx}) /\ (F " {y})) /\ ({ the Element of dx} /\ (F " {y})) by FUNCT_1:70
.= (((F " {y}) /\ (X \ { the Element of dx})) /\ { the Element of dx}) /\ (F " {y}) by XBOOLE_1:16
.= ((F " {y}) /\ ((X \ { the Element of dx}) /\ { the Element of dx})) /\ (F " {y}) by XBOOLE_1:16
.= {} /\ (F " {y}) by A14, XBOOLE_0:def_7
.= {} ;
hence card (Coim ((F | X),y)) = ((card ((F | (X \ { the Element of dx})) " {y})) + (card FF)) - (card {}) by A15, A19, CARD_2:45
.= card (Coim (A,y)) by A16, FINSEQ_3:57 ;
::_thesis: verum
end;
hence F | X,A are_fiberwise_equipotent by CLASSES1:def_9; ::_thesis: verum
end;
theorem :: RFINSEQ:5
for F being Function
for X being finite set ex f being FinSequence st F | X,f are_fiberwise_equipotent
proof
let F be Function; ::_thesis: for X being finite set ex f being FinSequence st F | X,f are_fiberwise_equipotent
let X be finite set ; ::_thesis: ex f being FinSequence st F | X,f are_fiberwise_equipotent
A1: card (dom (F | X)) = card (dom (F | X)) ;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(Lm1, Lm2);
hence ex f being FinSequence st F | X,f are_fiberwise_equipotent by A1; ::_thesis: verum
end;
definition
let n be Nat;
let f be FinSequence;
funcf /^ n -> FinSequence means :Def1: :: RFINSEQ:def 1
( len it = (len f) - n & ( for m being Nat st m in dom it holds
it . m = f . (m + n) ) ) if n <= len f
otherwise it = {} ;
existence
( ( n <= len f implies ex b1 being FinSequence st
( len b1 = (len f) - n & ( for m being Nat st m in dom b1 holds
b1 . m = f . (m + n) ) ) ) & ( not n <= len f implies ex b1 being FinSequence st b1 = {} ) )
proof
thus ( n <= len f implies ex p1 being FinSequence st
( len p1 = (len f) - n & ( for m being Nat st m in dom p1 holds
p1 . m = f . (m + n) ) ) ) ::_thesis: ( not n <= len f implies ex b1 being FinSequence st b1 = {} )
proof
assume n <= len f ; ::_thesis: ex p1 being FinSequence st
( len p1 = (len f) - n & ( for m being Nat st m in dom p1 holds
p1 . m = f . (m + n) ) )
then reconsider k = (len f) - n as Element of NAT by NAT_1:21;
deffunc H1( Nat) -> set = f . ($1 + n);
consider p being FinSequence such that
A1: ( len p = k & ( for m being Nat st m in dom p holds
p . m = H1(m) ) ) from FINSEQ_1:sch_2();
take p ; ::_thesis: ( len p = (len f) - n & ( for m being Nat st m in dom p holds
p . m = f . (m + n) ) )
thus len p = (len f) - n by A1; ::_thesis: for m being Nat st m in dom p holds
p . m = f . (m + n)
let m be Nat; ::_thesis: ( m in dom p implies p . m = f . (m + n) )
assume m in dom p ; ::_thesis: p . m = f . (m + n)
hence p . m = f . (m + n) by A1; ::_thesis: verum
end;
thus ( not n <= len f implies ex b1 being FinSequence st b1 = {} ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence holds
( ( n <= len f & len b1 = (len f) - n & ( for m being Nat st m in dom b1 holds
b1 . m = f . (m + n) ) & len b2 = (len f) - n & ( for m being Nat st m in dom b2 holds
b2 . m = f . (m + n) ) implies b1 = b2 ) & ( not n <= len f & b1 = {} & b2 = {} implies b1 = b2 ) )
proof
let p1, p2 be FinSequence; ::_thesis: ( ( n <= len f & len p1 = (len f) - n & ( for m being Nat st m in dom p1 holds
p1 . m = f . (m + n) ) & len p2 = (len f) - n & ( for m being Nat st m in dom p2 holds
p2 . m = f . (m + n) ) implies p1 = p2 ) & ( not n <= len f & p1 = {} & p2 = {} implies p1 = p2 ) )
thus ( n <= len f & len p1 = (len f) - n & ( for m being Nat st m in dom p1 holds
p1 . m = f . (m + n) ) & len p2 = (len f) - n & ( for m being Nat st m in dom p2 holds
p2 . m = f . (m + n) ) implies p1 = p2 ) ::_thesis: ( not n <= len f & p1 = {} & p2 = {} implies p1 = p2 )
proof
assume that
n <= len f and
A2: len p1 = (len f) - n and
A3: for m being Nat st m in dom p1 holds
p1 . m = f . (m + n) and
A4: len p2 = (len f) - n and
A5: for m being Nat st m in dom p2 holds
p2 . m = f . (m + n) ; ::_thesis: p1 = p2
A6: ( dom p1 = Seg (len p1) & Seg (len p2) = dom p2 ) by FINSEQ_1:def_3;
now__::_thesis:_for_m_being_Nat_st_m_in_dom_p1_holds_
p1_._m_=_p2_._m
let m be Nat; ::_thesis: ( m in dom p1 implies p1 . m = p2 . m )
assume A7: m in dom p1 ; ::_thesis: p1 . m = p2 . m
then p1 . m = f . (m + n) by A3;
hence p1 . m = p2 . m by A2, A4, A5, A6, A7; ::_thesis: verum
end;
hence p1 = p2 by A2, A4, FINSEQ_2:9; ::_thesis: verum
end;
thus ( not n <= len f & p1 = {} & p2 = {} implies p1 = p2 ) ; ::_thesis: verum
end;
consistency
for b1 being FinSequence holds verum ;
end;
:: deftheorem Def1 defines /^ RFINSEQ:def_1_:_
for n being Nat
for f, b3 being FinSequence holds
( ( n <= len f implies ( b3 = f /^ n iff ( len b3 = (len f) - n & ( for m being Nat st m in dom b3 holds
b3 . m = f . (m + n) ) ) ) ) & ( not n <= len f implies ( b3 = f /^ n iff b3 = {} ) ) );
definition
let D be set ;
let n be Nat;
let f be FinSequence of D;
:: original: /^
redefine funcf /^ n -> FinSequence of D;
coherence
f /^ n is FinSequence of D
proof
set p = f /^ n;
percases ( n <= len f or len f < n ) ;
supposeA1: n <= len f ; ::_thesis: f /^ n is FinSequence of D
then reconsider k = (len f) - n as Element of NAT by NAT_1:21;
A2: len (f /^ n) = k by A1, Def1;
rng (f /^ n) c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (f /^ n) or x in rng f )
assume x in rng (f /^ n) ; ::_thesis: x in rng f
then consider m being Nat such that
A3: m in dom (f /^ n) and
A4: (f /^ n) . m = x by FINSEQ_2:10;
m <= len (f /^ n) by A3, FINSEQ_3:25;
then A5: m + n <= len f by A2, XREAL_1:19;
A6: m <= m + n by NAT_1:11;
1 <= m by A3, FINSEQ_3:25;
then 1 <= m + n by A6, XXREAL_0:2;
then A7: m + n in dom f by A5, FINSEQ_3:25;
(f /^ n) . m = f . (m + n) by A1, A3, Def1;
hence x in rng f by A4, A7, FUNCT_1:def_3; ::_thesis: verum
end;
then rng (f /^ n) c= D by XBOOLE_1:1;
hence f /^ n is FinSequence of D by FINSEQ_1:def_4; ::_thesis: verum
end;
suppose len f < n ; ::_thesis: f /^ n is FinSequence of D
then f /^ n = <*> D by Def1;
hence f /^ n is FinSequence of D ; ::_thesis: verum
end;
end;
end;
end;
Lm3: for n being Nat
for D being non empty set
for f being FinSequence of D st len f <= n holds
f | n = f
proof
let n be Nat; ::_thesis: for D being non empty set
for f being FinSequence of D st len f <= n holds
f | n = f
let D be non empty set ; ::_thesis: for f being FinSequence of D st len f <= n holds
f | n = f
let f be FinSequence of D; ::_thesis: ( len f <= n implies f | n = f )
A1: dom f = Seg (len f) by FINSEQ_1:def_3;
assume len f <= n ; ::_thesis: f | n = f
then ( f | n = f | (Seg n) & dom f c= Seg n ) by A1, FINSEQ_1:5, FINSEQ_1:def_15;
hence f | n = f by RELAT_1:68; ::_thesis: verum
end;
theorem Th6: :: RFINSEQ:6
for D being non empty set
for f being FinSequence of D
for n, m being Nat st n in dom f & m in Seg n holds
( (f | n) . m = f . m & m in dom f )
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D
for n, m being Nat st n in dom f & m in Seg n holds
( (f | n) . m = f . m & m in dom f )
let f be FinSequence of D; ::_thesis: for n, m being Nat st n in dom f & m in Seg n holds
( (f | n) . m = f . m & m in dom f )
let n, m be Nat; ::_thesis: ( n in dom f & m in Seg n implies ( (f | n) . m = f . m & m in dom f ) )
assume that
A1: n in dom f and
A2: m in Seg n ; ::_thesis: ( (f | n) . m = f . m & m in dom f )
A3: f | n = f | (Seg n) by FINSEQ_1:def_15;
( dom f = Seg (len f) & n <= len f ) by A1, FINSEQ_1:def_3, FINSEQ_3:25;
then A4: Seg n c= dom f by FINSEQ_1:5;
then Seg n = (dom f) /\ (Seg n) by XBOOLE_1:28
.= dom (f | n) by A3, RELAT_1:61 ;
hence ( (f | n) . m = f . m & m in dom f ) by A2, A3, A4, FUNCT_1:47; ::_thesis: verum
end;
theorem Th7: :: RFINSEQ:7
for D being non empty set
for f being FinSequence of D
for n being Nat
for x being set st len f = n + 1 & x = f . (n + 1) holds
f = (f | n) ^ <*x*>
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D
for n being Nat
for x being set st len f = n + 1 & x = f . (n + 1) holds
f = (f | n) ^ <*x*>
let f be FinSequence of D; ::_thesis: for n being Nat
for x being set st len f = n + 1 & x = f . (n + 1) holds
f = (f | n) ^ <*x*>
let n be Nat; ::_thesis: for x being set st len f = n + 1 & x = f . (n + 1) holds
f = (f | n) ^ <*x*>
let x be set ; ::_thesis: ( len f = n + 1 & x = f . (n + 1) implies f = (f | n) ^ <*x*> )
assume that
A1: len f = n + 1 and
A2: x = f . (n + 1) ; ::_thesis: f = (f | n) ^ <*x*>
set fn = f | n;
A3: len (f | n) = n by A1, FINSEQ_1:59, NAT_1:11;
A4: dom f = Seg (len f) by FINSEQ_1:def_3;
A5: n <= n + 1 by NAT_1:11;
A6: now__::_thesis:_for_m_being_Nat_st_m_in_dom_f_holds_
f_._m_=_((f_|_n)_^_<*x*>)_._m
let m be Nat; ::_thesis: ( m in dom f implies f . m = ((f | n) ^ <*x*>) . m )
assume A7: m in dom f ; ::_thesis: f . m = ((f | n) ^ <*x*>) . m
then A8: 1 <= m by A4, FINSEQ_1:1;
A9: m <= len f by A4, A7, FINSEQ_1:1;
now__::_thesis:_(_(_m_=_len_f_&_f_._m_=_((f_|_n)_^_<*x*>)_._m_)_or_(_m_<>_len_f_&_((f_|_n)_^_<*x*>)_._m_=_f_._m_)_)
percases ( m = len f or m <> len f ) ;
case m = len f ; ::_thesis: f . m = ((f | n) ^ <*x*>) . m
hence f . m = ((f | n) ^ <*x*>) . m by A1, A2, A3, FINSEQ_1:42; ::_thesis: verum
end;
case m <> len f ; ::_thesis: ((f | n) ^ <*x*>) . m = f . m
then m < n + 1 by A1, A9, XXREAL_0:1;
then A10: m <= n by NAT_1:13;
then 1 <= n by A8, XXREAL_0:2;
then A11: n in dom f by A1, A5, FINSEQ_3:25;
A12: Seg (len (f | n)) = dom (f | n) by FINSEQ_1:def_3;
A13: m in dom (f | n) by A3, A8, A10, FINSEQ_3:25;
hence ((f | n) ^ <*x*>) . m = (f | n) . m by FINSEQ_1:def_7
.= f . m by A3, A13, A11, A12, Th6 ;
::_thesis: verum
end;
end;
end;
hence f . m = ((f | n) ^ <*x*>) . m ; ::_thesis: verum
end;
len ((f | n) ^ <*x*>) = n + (len <*x*>) by A3, FINSEQ_1:22
.= len f by A1, FINSEQ_1:40 ;
hence f = (f | n) ^ <*x*> by A6, FINSEQ_2:9; ::_thesis: verum
end;
theorem Th8: :: RFINSEQ:8
for D being non empty set
for f being FinSequence of D
for n being Nat holds (f | n) ^ (f /^ n) = f
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D
for n being Nat holds (f | n) ^ (f /^ n) = f
let f be FinSequence of D; ::_thesis: for n being Nat holds (f | n) ^ (f /^ n) = f
let n be Nat; ::_thesis: (f | n) ^ (f /^ n) = f
set fn = f /^ n;
now__::_thesis:_(_(_len_f_<_n_&_(f_|_n)_^_(f_/^_n)_=_f_)_or_(_n_<=_len_f_&_(f_|_n)_^_(f_/^_n)_=_f_)_)
percases ( len f < n or n <= len f ) ;
case len f < n ; ::_thesis: (f | n) ^ (f /^ n) = f
then ( f /^ n = <*> D & f | n = f ) by Def1, Lm3;
hence (f | n) ^ (f /^ n) = f by FINSEQ_1:34; ::_thesis: verum
end;
caseA1: n <= len f ; ::_thesis: (f | n) ^ (f /^ n) = f
A2: dom f = Seg (len f) by FINSEQ_1:def_3;
A3: len (f | n) = n by A1, FINSEQ_1:59;
A4: len (f /^ n) = (len f) - n by A1, Def1;
then A5: len ((f | n) ^ (f /^ n)) = n + ((len f) - n) by A3, FINSEQ_1:22
.= len f ;
A6: dom (f | n) = Seg n by A3, FINSEQ_1:def_3;
now__::_thesis:_for_m_being_Nat_st_m_in_dom_f_holds_
((f_|_n)_^_(f_/^_n))_._m_=_f_._m
let m be Nat; ::_thesis: ( m in dom f implies ((f | n) ^ (f /^ n)) . m = f . m )
assume A7: m in dom f ; ::_thesis: ((f | n) ^ (f /^ n)) . m = f . m
then A8: m <= len f by A2, FINSEQ_1:1;
A9: 1 <= m by A2, A7, FINSEQ_1:1;
now__::_thesis:_(_(_m_<=_n_&_((f_|_n)_^_(f_/^_n))_._m_=_f_._m_)_or_(_n_<_m_&_((f_|_n)_^_(f_/^_n))_._m_=_f_._m_)_)
percases ( m <= n or n < m ) ;
caseA10: m <= n ; ::_thesis: ((f | n) ^ (f /^ n)) . m = f . m
then 1 <= n by A9, XXREAL_0:2;
then A11: n in dom f by A1, FINSEQ_3:25;
A12: m in Seg n by A9, A10, FINSEQ_1:1;
hence ((f | n) ^ (f /^ n)) . m = (f | n) . m by A6, FINSEQ_1:def_7
.= f . m by A12, A11, Th6 ;
::_thesis: verum
end;
caseA13: n < m ; ::_thesis: ((f | n) ^ (f /^ n)) . m = f . m
then max (0,(m - n)) = m - n by FINSEQ_2:4;
then reconsider k = m - n as Element of NAT by FINSEQ_2:5;
n + 1 <= m by A13, NAT_1:13;
then A14: 1 <= k by XREAL_1:19;
k <= len (f /^ n) by A4, A8, XREAL_1:9;
then A15: k in dom (f /^ n) by A14, FINSEQ_3:25;
thus ((f | n) ^ (f /^ n)) . m = (f /^ n) . k by A3, A5, A8, A13, FINSEQ_1:24
.= f . (k + n) by A1, A15, Def1
.= f . m ; ::_thesis: verum
end;
end;
end;
hence ((f | n) ^ (f /^ n)) . m = f . m ; ::_thesis: verum
end;
hence (f | n) ^ (f /^ n) = f by A5, FINSEQ_2:9; ::_thesis: verum
end;
end;
end;
hence (f | n) ^ (f /^ n) = f ; ::_thesis: verum
end;
theorem :: RFINSEQ:9
for R1, R2 being FinSequence of REAL st R1,R2 are_fiberwise_equipotent holds
Sum R1 = Sum R2
proof
let R1, R2 be FinSequence of REAL ; ::_thesis: ( R1,R2 are_fiberwise_equipotent implies Sum R1 = Sum R2 )
defpred S2[ Nat] means for f, g being FinSequence of REAL st f,g are_fiberwise_equipotent & len f = $1 holds
Sum f = Sum g;
assume A1: R1,R2 are_fiberwise_equipotent ; ::_thesis: Sum R1 = Sum R2
A2: len R1 = len R1 ;
A3: for n being Element of NAT st S2[n] holds
S2[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] )
assume A4: S2[n] ; ::_thesis: S2[n + 1]
let f, g be FinSequence of REAL ; ::_thesis: ( f,g are_fiberwise_equipotent & len f = n + 1 implies Sum f = Sum g )
assume that
A5: f,g are_fiberwise_equipotent and
A6: len f = n + 1 ; ::_thesis: Sum f = Sum g
set a = f . (n + 1);
A7: rng f = rng g by A5, CLASSES1:75;
0 < n + 1 by NAT_1:3;
then 0 + 1 <= n + 1 by NAT_1:13;
then n + 1 in dom f by A6, FINSEQ_3:25;
then f . (n + 1) in rng g by A7, FUNCT_1:def_3;
then consider m being Nat such that
A8: m in dom g and
A9: g . m = f . (n + 1) by FINSEQ_2:10;
set gg = g /^ m;
set gm = g | m;
m <= len g by A8, FINSEQ_3:25;
then A10: len (g | m) = m by FINSEQ_1:59;
A11: 1 <= m by A8, FINSEQ_3:25;
then max (0,(m - 1)) = m - 1 by FINSEQ_2:4;
then reconsider m1 = m - 1 as Element of NAT by FINSEQ_2:5;
A12: m = m1 + 1 ;
then m1 <= m by NAT_1:11;
then A13: Seg m1 c= Seg m by FINSEQ_1:5;
m in Seg m by A11, FINSEQ_1:1;
then (g | m) . m = f . (n + 1) by A8, A9, Th6;
then A14: g | m = ((g | m) | m1) ^ <*(f . (n + 1))*> by A10, A12, Th7;
set fn = f | n;
A15: g = (g | m) ^ (g /^ m) by Th8;
A16: (g | m) | m1 = (g | m) | (Seg m1) by FINSEQ_1:def_15
.= (g | (Seg m)) | (Seg m1) by FINSEQ_1:def_15
.= g | ((Seg m) /\ (Seg m1)) by RELAT_1:71
.= g | (Seg m1) by A13, XBOOLE_1:28
.= g | m1 by FINSEQ_1:def_15 ;
A17: f = (f | n) ^ <*(f . (n + 1))*> by A6, Th7;
now__::_thesis:_for_x_being_set_holds_card_(Coim_((f_|_n),x))_=_card_(Coim_(((g_|_m1)_^_(g_/^_m)),x))
let x be set ; ::_thesis: card (Coim ((f | n),x)) = card (Coim (((g | m1) ^ (g /^ m)),x))
card (Coim (f,x)) = card (Coim (g,x)) by A5, CLASSES1:def_9;
then (card ((f | n) " {x})) + (card (<*(f . (n + 1))*> " {x})) = card ((((g | m1) ^ <*(f . (n + 1))*>) ^ (g /^ m)) " {x}) by A15, A14, A16, A17, FINSEQ_3:57
.= (card (((g | m1) ^ <*(f . (n + 1))*>) " {x})) + (card ((g /^ m) " {x})) by FINSEQ_3:57
.= ((card ((g | m1) " {x})) + (card (<*(f . (n + 1))*> " {x}))) + (card ((g /^ m) " {x})) by FINSEQ_3:57
.= ((card ((g | m1) " {x})) + (card ((g /^ m) " {x}))) + (card (<*(f . (n + 1))*> " {x}))
.= (card (((g | m1) ^ (g /^ m)) " {x})) + (card (<*(f . (n + 1))*> " {x})) by FINSEQ_3:57 ;
hence card (Coim ((f | n),x)) = card (Coim (((g | m1) ^ (g /^ m)),x)) ; ::_thesis: verum
end;
then A18: f | n,(g | m1) ^ (g /^ m) are_fiberwise_equipotent by CLASSES1:def_9;
len (f | n) = n by A6, FINSEQ_1:59, NAT_1:11;
then Sum (f | n) = Sum ((g | m1) ^ (g /^ m)) by A4, A18;
hence Sum f = (Sum ((g | m1) ^ (g /^ m))) + (Sum <*(f . (n + 1))*>) by A17, RVSUM_1:75
.= ((Sum (g | m1)) + (Sum (g /^ m))) + (Sum <*(f . (n + 1))*>) by RVSUM_1:75
.= ((Sum (g | m1)) + (Sum <*(f . (n + 1))*>)) + (Sum (g /^ m))
.= (Sum (g | m)) + (Sum (g /^ m)) by A14, A16, RVSUM_1:75
.= Sum g by A15, RVSUM_1:75 ;
::_thesis: verum
end;
A19: S2[ 0 ]
proof
let f, g be FinSequence of REAL ; ::_thesis: ( f,g are_fiberwise_equipotent & len f = 0 implies Sum f = Sum g )
assume ( f,g are_fiberwise_equipotent & len f = 0 ) ; ::_thesis: Sum f = Sum g
then A20: ( len g = 0 & f = <*> REAL ) by Th3;
then g = <*> REAL ;
hence Sum f = Sum g by A20; ::_thesis: verum
end;
for n being Element of NAT holds S2[n] from NAT_1:sch_1(A19, A3);
hence Sum R1 = Sum R2 by A1, A2; ::_thesis: verum
end;
definition
let R be FinSequence of REAL ;
func MIM R -> FinSequence of REAL means :Def2: :: RFINSEQ:def 2
( len it = len R & it . (len it) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len it) - 1 holds
it . n = (R . n) - (R . (n + 1)) ) );
existence
ex b1 being FinSequence of REAL st
( len b1 = len R & b1 . (len b1) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len b1) - 1 holds
b1 . n = (R . n) - (R . (n + 1)) ) )
proof
percases ( len R = 0 or len R <> 0 ) ;
supposeA1: len R = 0 ; ::_thesis: ex b1 being FinSequence of REAL st
( len b1 = len R & b1 . (len b1) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len b1) - 1 holds
b1 . n = (R . n) - (R . (n + 1)) ) )
take a = R; ::_thesis: ( len a = len R & a . (len a) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len a) - 1 holds
a . n = (R . n) - (R . (n + 1)) ) )
thus ( len a = len R & a . (len a) = R . (len R) ) ; ::_thesis: for n being Nat st 1 <= n & n <= (len a) - 1 holds
a . n = (R . n) - (R . (n + 1))
let n be Nat; ::_thesis: ( 1 <= n & n <= (len a) - 1 implies a . n = (R . n) - (R . (n + 1)) )
assume ( 1 <= n & n <= (len a) - 1 ) ; ::_thesis: a . n = (R . n) - (R . (n + 1))
hence a . n = (R . n) - (R . (n + 1)) by A1, XXREAL_0:2; ::_thesis: verum
end;
suppose len R <> 0 ; ::_thesis: ex b1 being FinSequence of REAL st
( len b1 = len R & b1 . (len b1) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len b1) - 1 holds
b1 . n = (R . n) - (R . (n + 1)) ) )
then 0 < len R by NAT_1:3;
then 0 + 1 <= len R by NAT_1:13;
then max (0,((len R) - 1)) = (len R) - 1 by FINSEQ_2:4;
then reconsider l = (len R) - 1 as Element of NAT by FINSEQ_2:5;
defpred S2[ Nat, set ] means $2 = (R . $1) - (R . ($1 + 1));
set t = R . (len R);
A2: for n being Nat st n in Seg l holds
ex x being Real st S2[n,x] ;
consider p being FinSequence of REAL such that
A3: ( dom p = Seg l & ( for n being Nat st n in Seg l holds
S2[n,p . n] ) ) from FINSEQ_1:sch_5(A2);
take a = p ^ <*(R . (len R))*>; ::_thesis: ( len a = len R & a . (len a) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len a) - 1 holds
a . n = (R . n) - (R . (n + 1)) ) )
thus A4: len a = (len p) + (len <*(R . (len R))*>) by FINSEQ_1:22
.= l + (len <*(R . (len R))*>) by A3, FINSEQ_1:def_3
.= l + 1 by FINSEQ_1:39
.= len R ; ::_thesis: ( a . (len a) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len a) - 1 holds
a . n = (R . n) - (R . (n + 1)) ) )
hence a . (len a) = a . (l + 1)
.= a . ((len p) + 1) by A3, FINSEQ_1:def_3
.= R . (len R) by FINSEQ_1:42 ;
::_thesis: for n being Nat st 1 <= n & n <= (len a) - 1 holds
a . n = (R . n) - (R . (n + 1))
let n be Nat; ::_thesis: ( 1 <= n & n <= (len a) - 1 implies a . n = (R . n) - (R . (n + 1)) )
assume ( 1 <= n & n <= (len a) - 1 ) ; ::_thesis: a . n = (R . n) - (R . (n + 1))
then A5: n in Seg l by A4, FINSEQ_1:1;
then p . n = (R . n) - (R . (n + 1)) by A3;
hence a . n = (R . n) - (R . (n + 1)) by A3, A5, FINSEQ_1:def_7; ::_thesis: verum
end;
end;
end;
uniqueness
for b1, b2 being FinSequence of REAL st len b1 = len R & b1 . (len b1) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len b1) - 1 holds
b1 . n = (R . n) - (R . (n + 1)) ) & len b2 = len R & b2 . (len b2) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len b2) - 1 holds
b2 . n = (R . n) - (R . (n + 1)) ) holds
b1 = b2
proof
let p1, p2 be FinSequence of REAL ; ::_thesis: ( len p1 = len R & p1 . (len p1) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len p1) - 1 holds
p1 . n = (R . n) - (R . (n + 1)) ) & len p2 = len R & p2 . (len p2) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len p2) - 1 holds
p2 . n = (R . n) - (R . (n + 1)) ) implies p1 = p2 )
assume that
A6: len p1 = len R and
A7: p1 . (len p1) = R . (len R) and
A8: for n being Nat st 1 <= n & n <= (len p1) - 1 holds
p1 . n = (R . n) - (R . (n + 1)) and
A9: len p2 = len R and
A10: p2 . (len p2) = R . (len R) and
A11: for n being Nat st 1 <= n & n <= (len p2) - 1 holds
p2 . n = (R . n) - (R . (n + 1)) ; ::_thesis: p1 = p2
A12: dom p1 = Seg (len R) by A6, FINSEQ_1:def_3;
now__::_thesis:_for_n_being_Nat_st_n_in_dom_p1_holds_
p1_._n_=_p2_._n
let n be Nat; ::_thesis: ( n in dom p1 implies p1 . n = p2 . n )
set r = R . n;
assume A13: n in dom p1 ; ::_thesis: p1 . n = p2 . n
then A14: 1 <= n by A12, FINSEQ_1:1;
A15: n <= len R by A12, A13, FINSEQ_1:1;
now__::_thesis:_(_(_n_=_len_R_&_p1_._n_=_p2_._n_)_or_(_n_<>_len_R_&_p1_._n_=_p2_._n_)_)
percases ( n = len R or n <> len R ) ;
case n = len R ; ::_thesis: p1 . n = p2 . n
hence p1 . n = p2 . n by A6, A7, A9, A10; ::_thesis: verum
end;
caseA16: n <> len R ; ::_thesis: p1 . n = p2 . n
set s = R . (n + 1);
n < len R by A15, A16, XXREAL_0:1;
then n + 1 <= len R by NAT_1:13;
then A17: n <= (len R) - 1 by XREAL_1:19;
then p1 . n = (R . n) - (R . (n + 1)) by A6, A8, A14;
hence p1 . n = p2 . n by A9, A11, A14, A17; ::_thesis: verum
end;
end;
end;
hence p1 . n = p2 . n ; ::_thesis: verum
end;
hence p1 = p2 by A6, A9, FINSEQ_2:9; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines MIM RFINSEQ:def_2_:_
for R, b2 being FinSequence of REAL holds
( b2 = MIM R iff ( len b2 = len R & b2 . (len b2) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len b2) - 1 holds
b2 . n = (R . n) - (R . (n + 1)) ) ) );
theorem Th10: :: RFINSEQ:10
for R being FinSequence of REAL
for r being Real
for n being Element of NAT st len R = n + 2 & R . (n + 1) = r holds
MIM (R | (n + 1)) = ((MIM R) | n) ^ <*r*>
proof
let R be FinSequence of REAL ; ::_thesis: for r being Real
for n being Element of NAT st len R = n + 2 & R . (n + 1) = r holds
MIM (R | (n + 1)) = ((MIM R) | n) ^ <*r*>
let s be Real; ::_thesis: for n being Element of NAT st len R = n + 2 & R . (n + 1) = s holds
MIM (R | (n + 1)) = ((MIM R) | n) ^ <*s*>
let n be Element of NAT ; ::_thesis: ( len R = n + 2 & R . (n + 1) = s implies MIM (R | (n + 1)) = ((MIM R) | n) ^ <*s*> )
assume that
A1: len R = n + 2 and
A2: R . (n + 1) = s ; ::_thesis: MIM (R | (n + 1)) = ((MIM R) | n) ^ <*s*>
set f1 = R | (n + 1);
set m1 = MIM (R | (n + 1));
set mf = MIM R;
set fn = (MIM R) | n;
0 < n + 1 by NAT_1:3;
then A3: 0 + 1 <= n + 1 by NAT_1:13;
A4: (n + 1) + 1 = n + (1 + 1) ;
then n + 1 <= n + 2 by NAT_1:11;
then A5: ( Seg (len R) = dom R & n + 1 in Seg (n + 2) ) by A3, FINSEQ_1:1, FINSEQ_1:def_3;
A6: len (R | (n + 1)) = n + 1 by A1, A4, FINSEQ_1:59, NAT_1:11;
then A7: len (MIM (R | (n + 1))) = n + 1 by Def2;
then A8: dom (MIM (R | (n + 1))) = Seg (n + 1) by FINSEQ_1:def_3;
n + 1 in Seg (n + 1) by A3, FINSEQ_1:1;
then (R | (n + 1)) . (n + 1) = s by A1, A2, A5, Th6;
then A9: (MIM (R | (n + 1))) . (n + 1) = s by A6, A7, Def2;
A10: Seg (len ((MIM R) | n)) = dom ((MIM R) | n) by FINSEQ_1:def_3;
A11: Seg (len (MIM R)) = dom (MIM R) by FINSEQ_1:def_3;
A12: len (MIM R) = n + 2 by A1, Def2;
then A13: len ((MIM R) | n) = n by FINSEQ_1:59, NAT_1:11;
A14: n <= n + 2 by NAT_1:11;
A15: now__::_thesis:_for_m_being_Nat_st_m_in_dom_(MIM_(R_|_(n_+_1)))_holds_
(MIM_(R_|_(n_+_1)))_._m_=_(((MIM_R)_|_n)_^_<*s*>)_._m
let m be Nat; ::_thesis: ( m in dom (MIM (R | (n + 1))) implies (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m )
assume A16: m in dom (MIM (R | (n + 1))) ; ::_thesis: (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m
then A17: 1 <= m by A8, FINSEQ_1:1;
A18: m <= n + 1 by A8, A16, FINSEQ_1:1;
now__::_thesis:_(_(_m_=_n_+_1_&_(MIM_(R_|_(n_+_1)))_._m_=_(((MIM_R)_|_n)_^_<*s*>)_._m_)_or_(_m_<>_n_+_1_&_(MIM_(R_|_(n_+_1)))_._m_=_(((MIM_R)_|_n)_^_<*s*>)_._m_)_)
percases ( m = n + 1 or m <> n + 1 ) ;
case m = n + 1 ; ::_thesis: (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m
hence (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m by A13, A9, FINSEQ_1:42; ::_thesis: verum
end;
case m <> n + 1 ; ::_thesis: (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m
then A19: m < n + 1 by A18, XXREAL_0:1;
then A20: m <= n by NAT_1:13;
then A21: m in Seg n by A17, FINSEQ_1:1;
set r2 = R . (m + 1);
set r1 = R . m;
A22: (len (MIM R)) - 1 = n + 1 by A12;
1 <= n by A17, A20, XXREAL_0:2;
then n in Seg (n + 2) by A14, FINSEQ_1:1;
then ((MIM R) | n) . m = (MIM R) . m by A12, A11, A21, Th6;
then A23: (R . m) - (R . (m + 1)) = ((MIM R) | n) . m by A17, A18, A22, Def2
.= (((MIM R) | n) ^ <*s*>) . m by A13, A10, A21, FINSEQ_1:def_7 ;
( 1 <= m + 1 & m + 1 <= n + 1 ) by A19, NAT_1:11, NAT_1:13;
then m + 1 in Seg (n + 1) by FINSEQ_1:1;
then A24: (R | (n + 1)) . (m + 1) = R . (m + 1) by A1, A5, Th6;
( (len (MIM (R | (n + 1)))) - 1 = n & (R | (n + 1)) . m = R . m ) by A1, A7, A5, A8, A16, Th6;
hence (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m by A17, A20, A23, A24, Def2; ::_thesis: verum
end;
end;
end;
hence (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m ; ::_thesis: verum
end;
len (((MIM R) | n) ^ <*s*>) = n + (len <*s*>) by A13, FINSEQ_1:22
.= n + 1 by FINSEQ_1:40 ;
hence MIM (R | (n + 1)) = ((MIM R) | n) ^ <*s*> by A7, A15, FINSEQ_2:9; ::_thesis: verum
end;
theorem Th11: :: RFINSEQ:11
for R being FinSequence of REAL
for r, s being Real
for n being Element of NAT st len R = n + 2 & R . (n + 1) = r & R . (n + 2) = s holds
MIM R = ((MIM R) | n) ^ <*(r - s),s*>
proof
let R be FinSequence of REAL ; ::_thesis: for r, s being Real
for n being Element of NAT st len R = n + 2 & R . (n + 1) = r & R . (n + 2) = s holds
MIM R = ((MIM R) | n) ^ <*(r - s),s*>
let r, s be Real; ::_thesis: for n being Element of NAT st len R = n + 2 & R . (n + 1) = r & R . (n + 2) = s holds
MIM R = ((MIM R) | n) ^ <*(r - s),s*>
let n be Element of NAT ; ::_thesis: ( len R = n + 2 & R . (n + 1) = r & R . (n + 2) = s implies MIM R = ((MIM R) | n) ^ <*(r - s),s*> )
set mf = MIM R;
set nf = (MIM R) | n;
assume that
A1: len R = n + 2 and
A2: R . (n + 1) = r and
A3: R . (n + 2) = s ; ::_thesis: MIM R = ((MIM R) | n) ^ <*(r - s),s*>
A4: len (MIM R) = n + 2 by A1, Def2;
then A5: dom (MIM R) = Seg (n + 2) by FINSEQ_1:def_3;
A6: n + (1 + 1) = (n + 1) + 1 ;
then n + 1 <= n + 2 by NAT_1:11;
then A7: n < n + 2 by NAT_1:13;
A8: len ((MIM R) | n) = n by A4, FINSEQ_1:59, NAT_1:11;
then len (((MIM R) | n) ^ <*(r - s),s*>) = n + (len <*(r - s),s*>) by FINSEQ_1:22;
then A9: len (((MIM R) | n) ^ <*(r - s),s*>) = n + 2 by FINSEQ_1:44;
A10: n <= n + 2 by NAT_1:11;
now__::_thesis:_for_m_being_Nat_st_m_in_dom_(MIM_R)_holds_
(MIM_R)_._m_=_(((MIM_R)_|_n)_^_<*(r_-_s),s*>)_._m
let m be Nat; ::_thesis: ( m in dom (MIM R) implies (MIM R) . m = (((MIM R) | n) ^ <*(r - s),s*>) . m )
assume A11: m in dom (MIM R) ; ::_thesis: (MIM R) . m = (((MIM R) | n) ^ <*(r - s),s*>) . m
then A12: 1 <= m by A5, FINSEQ_1:1;
A13: m <= n + 2 by A5, A11, FINSEQ_1:1;
now__::_thesis:_(_(_m_=_n_+_2_&_(MIM_R)_._m_=_(((MIM_R)_|_n)_^_<*(r_-_s),s*>)_._m_)_or_(_m_<>_n_+_2_&_(MIM_R)_._m_=_(((MIM_R)_|_n)_^_<*(r_-_s),s*>)_._m_)_)
percases ( m = n + 2 or m <> n + 2 ) ;
caseA14: m = n + 2 ; ::_thesis: (MIM R) . m = (((MIM R) | n) ^ <*(r - s),s*>) . m
hence (MIM R) . m = s by A1, A3, A4, Def2
.= <*(r - s),s*> . ((n + 2) - n) by FINSEQ_1:44
.= (((MIM R) | n) ^ <*(r - s),s*>) . m by A8, A9, A7, A14, FINSEQ_1:24 ;
::_thesis: verum
end;
case m <> n + 2 ; ::_thesis: (MIM R) . m = (((MIM R) | n) ^ <*(r - s),s*>) . m
then m < n + 2 by A13, XXREAL_0:1;
then A15: m <= n + 1 by A6, NAT_1:13;
A16: (len (MIM R)) - 1 = n + 1 by A4;
now__::_thesis:_(_(_m_=_n_+_1_&_(MIM_R)_._m_=_(((MIM_R)_|_n)_^_<*(r_-_s),s*>)_._m_)_or_(_m_<>_n_+_1_&_(MIM_R)_._m_=_(((MIM_R)_|_n)_^_<*(r_-_s),s*>)_._m_)_)
percases ( m = n + 1 or m <> n + 1 ) ;
caseA17: m = n + 1 ; ::_thesis: (MIM R) . m = (((MIM R) | n) ^ <*(r - s),s*>) . m
then A18: n < m by NAT_1:13;
thus (MIM R) . m = r - s by A2, A3, A6, A12, A16, A17, Def2
.= <*(r - s),s*> . ((n + 1) - n) by FINSEQ_1:44
.= (((MIM R) | n) ^ <*(r - s),s*>) . m by A8, A9, A13, A17, A18, FINSEQ_1:24 ; ::_thesis: verum
end;
case m <> n + 1 ; ::_thesis: (MIM R) . m = (((MIM R) | n) ^ <*(r - s),s*>) . m
then m < n + 1 by A15, XXREAL_0:1;
then A19: m <= n by NAT_1:13;
then A20: m in Seg n by A12, FINSEQ_1:1;
1 <= n by A12, A19, XXREAL_0:2;
then A21: n in Seg (n + 2) by A10, FINSEQ_1:1;
A22: dom ((MIM R) | n) = Seg (len ((MIM R) | n)) by FINSEQ_1:def_3;
dom (MIM R) = Seg (len (MIM R)) by FINSEQ_1:def_3;
hence (MIM R) . m = ((MIM R) | n) . m by A4, A20, A21, Th6
.= (((MIM R) | n) ^ <*(r - s),s*>) . m by A8, A20, A22, FINSEQ_1:def_7 ;
::_thesis: verum
end;
end;
end;
hence (MIM R) . m = (((MIM R) | n) ^ <*(r - s),s*>) . m ; ::_thesis: verum
end;
end;
end;
hence (MIM R) . m = (((MIM R) | n) ^ <*(r - s),s*>) . m ; ::_thesis: verum
end;
hence MIM R = ((MIM R) | n) ^ <*(r - s),s*> by A4, A9, FINSEQ_2:9; ::_thesis: verum
end;
theorem Th12: :: RFINSEQ:12
MIM (<*> REAL) = <*> REAL
proof
set o = <*> REAL;
set mo = MIM (<*> REAL);
len (MIM (<*> REAL)) = len (<*> REAL) by Def2;
hence MIM (<*> REAL) = <*> REAL ; ::_thesis: verum
end;
theorem Th13: :: RFINSEQ:13
for r being Real holds MIM <*r*> = <*r*>
proof
let r be Real; ::_thesis: MIM <*r*> = <*r*>
set f = <*r*>;
A1: len <*r*> = 1 by FINSEQ_1:40;
then A2: len (MIM <*r*>) = 1 by Def2;
then A3: dom (MIM <*r*>) = Seg 1 by FINSEQ_1:def_3;
now__::_thesis:_for_n_being_Nat_st_n_in_dom_(MIM_<*r*>)_holds_
(MIM_<*r*>)_._n_=_<*r*>_._n
let n be Nat; ::_thesis: ( n in dom (MIM <*r*>) implies (MIM <*r*>) . n = <*r*> . n )
assume n in dom (MIM <*r*>) ; ::_thesis: (MIM <*r*>) . n = <*r*> . n
then n = 1 by A3, FINSEQ_1:2, TARSKI:def_1;
hence (MIM <*r*>) . n = <*r*> . n by A1, A2, Def2; ::_thesis: verum
end;
hence MIM <*r*> = <*r*> by A1, A2, FINSEQ_2:9; ::_thesis: verum
end;
theorem :: RFINSEQ:14
for r, s being Real holds MIM <*r,s*> = <*(r - s),s*>
proof
let r, s be Real; ::_thesis: MIM <*r,s*> = <*(r - s),s*>
set f = <*r,s*>;
A1: ( len <*r,s*> = 2 & <*r,s*> . 1 = r ) by FINSEQ_1:44;
A2: <*r,s*> . 2 = s by FINSEQ_1:44;
( 0 + 2 = 2 & 0 + 1 = 1 ) ;
then MIM <*r,s*> = ((MIM <*r,s*>) | 0) ^ <*(r - s),s*> by A1, A2, Th11;
hence MIM <*r,s*> = <*(r - s),s*> by FINSEQ_1:34; ::_thesis: verum
end;
theorem :: RFINSEQ:15
for R being FinSequence of REAL
for n being Element of NAT holds (MIM R) /^ n = MIM (R /^ n)
proof
let R be FinSequence of REAL ; ::_thesis: for n being Element of NAT holds (MIM R) /^ n = MIM (R /^ n)
let n be Element of NAT ; ::_thesis: (MIM R) /^ n = MIM (R /^ n)
set mf = MIM R;
set fn = R /^ n;
set mn = MIM (R /^ n);
A1: len (MIM R) = len R by Def2;
A2: len (MIM (R /^ n)) = len (R /^ n) by Def2;
now__::_thesis:_(_(_len_R_<_n_&_(MIM_R)_/^_n_=_MIM_(R_/^_n)_)_or_(_n_<=_len_R_&_(MIM_R)_/^_n_=_MIM_(R_/^_n)_)_)
percases ( len R < n or n <= len R ) ;
caseA3: len R < n ; ::_thesis: (MIM R) /^ n = MIM (R /^ n)
then (MIM R) /^ n = <*> REAL by A1, Def1;
hence (MIM R) /^ n = MIM (R /^ n) by A3, Def1, Th12; ::_thesis: verum
end;
caseA4: n <= len R ; ::_thesis: (MIM R) /^ n = MIM (R /^ n)
then A5: len ((MIM R) /^ n) = (len R) - n by A1, Def1;
A6: len (MIM (R /^ n)) = len (R /^ n) by Def2;
then A7: dom (MIM (R /^ n)) = Seg (len (R /^ n)) by FINSEQ_1:def_3;
A8: Seg (len ((MIM R) /^ n)) = dom ((MIM R) /^ n) by FINSEQ_1:def_3;
A9: len (R /^ n) = (len R) - n by A4, Def1;
A10: Seg (len (R /^ n)) = dom (R /^ n) by FINSEQ_1:def_3;
now__::_thesis:_for_m_being_Nat_st_m_in_dom_(MIM_(R_/^_n))_holds_
((MIM_R)_/^_n)_._m_=_(MIM_(R_/^_n))_._m
let m be Nat; ::_thesis: ( m in dom (MIM (R /^ n)) implies ((MIM R) /^ n) . m = (MIM (R /^ n)) . m )
set r1 = R . (m + n);
assume A11: m in dom (MIM (R /^ n)) ; ::_thesis: ((MIM R) /^ n) . m = (MIM (R /^ n)) . m
then A12: 1 <= m by A7, FINSEQ_1:1;
A13: m <= len (R /^ n) by A7, A11, FINSEQ_1:1;
A14: (R /^ n) . m = R . (m + n) by A4, A10, A7, A11, Def1;
m <= m + n by NAT_1:11;
then A15: 1 <= m + n by A12, XXREAL_0:2;
now__::_thesis:_(_(_m_=_len_(R_/^_n)_&_((MIM_R)_/^_n)_._m_=_(MIM_(R_/^_n))_._m_)_or_(_m_<>_len_(R_/^_n)_&_((MIM_R)_/^_n)_._m_=_(MIM_(R_/^_n))_._m_)_)
percases ( m = len (R /^ n) or m <> len (R /^ n) ) ;
caseA16: m = len (R /^ n) ; ::_thesis: ((MIM R) /^ n) . m = (MIM (R /^ n)) . m
thus ((MIM R) /^ n) . m = (MIM R) . (m + n) by A1, A4, A5, A9, A8, A7, A11, Def1
.= R . (m + n) by A1, A9, A16, Def2
.= (MIM (R /^ n)) . m by A6, A14, A16, Def2 ; ::_thesis: verum
end;
case m <> len (R /^ n) ; ::_thesis: ((MIM R) /^ n) . m = (MIM (R /^ n)) . m
then m < len (R /^ n) by A13, XXREAL_0:1;
then A17: m + 1 <= len (R /^ n) by NAT_1:13;
then A18: m <= (len (R /^ n)) - 1 by XREAL_1:19;
set r2 = R . ((m + 1) + n);
A19: (m + 1) + n = (m + n) + 1 ;
1 <= m + 1 by NAT_1:11;
then m + 1 in dom (R /^ n) by A17, FINSEQ_3:25;
then A20: (R /^ n) . (m + 1) = R . ((m + 1) + n) by A4, Def1;
(m + 1) + n <= len R by A9, A17, XREAL_1:19;
then A21: m + n <= (len R) - 1 by A19, XREAL_1:19;
thus ((MIM R) /^ n) . m = (MIM R) . (m + n) by A1, A4, A5, A9, A8, A7, A11, Def1
.= (R . (m + n)) - (R . ((m + 1) + n)) by A1, A15, A19, A21, Def2
.= (MIM (R /^ n)) . m by A2, A12, A14, A18, A20, Def2 ; ::_thesis: verum
end;
end;
end;
hence ((MIM R) /^ n) . m = (MIM (R /^ n)) . m ; ::_thesis: verum
end;
hence (MIM R) /^ n = MIM (R /^ n) by A5, A9, A6, FINSEQ_2:9; ::_thesis: verum
end;
end;
end;
hence (MIM R) /^ n = MIM (R /^ n) ; ::_thesis: verum
end;
theorem Th16: :: RFINSEQ:16
for R being FinSequence of REAL st len R <> 0 holds
Sum (MIM R) = R . 1
proof
defpred S2[ Nat] means for R being FinSequence of REAL st len R <> 0 & len R = $1 holds
Sum (MIM R) = R . 1;
let R be FinSequence of REAL ; ::_thesis: ( len R <> 0 implies Sum (MIM R) = R . 1 )
assume A1: len R <> 0 ; ::_thesis: Sum (MIM R) = R . 1
A2: for n being Element of NAT st S2[n] holds
S2[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] )
assume A3: S2[n] ; ::_thesis: S2[n + 1]
let R be FinSequence of REAL ; ::_thesis: ( len R <> 0 & len R = n + 1 implies Sum (MIM R) = R . 1 )
assume that
len R <> 0 and
A4: len R = n + 1 ; ::_thesis: Sum (MIM R) = R . 1
now__::_thesis:_(_(_n_=_0_&_Sum_(MIM_R)_=_R_._1_)_or_(_n_<>_0_&_Sum_(MIM_R)_=_R_._1_)_)
percases ( n = 0 or n <> 0 ) ;
case n = 0 ; ::_thesis: Sum (MIM R) = R . 1
then A5: R = <*(R . 1)*> by A4, FINSEQ_1:40;
then MIM R = R by Th13;
hence Sum (MIM R) = R . 1 by A5, FINSOP_1:11; ::_thesis: verum
end;
case n <> 0 ; ::_thesis: Sum (MIM R) = R . 1
then 0 < n by NAT_1:3;
then 0 + 1 <= n by NAT_1:13;
then max (0,(n - 1)) = n - 1 by FINSEQ_2:4;
then reconsider n1 = n - 1 as Element of NAT by FINSEQ_2:5;
A6: 0 + 1 <= n1 + 1 by NAT_1:11;
then A7: ( Seg (len R) = dom R & 1 in Seg (n1 + 1) ) by FINSEQ_1:1, FINSEQ_1:def_3;
n1 + 2 = (n1 + 1) + 1 ;
then n1 + 1 <= n1 + 2 by NAT_1:11;
then A8: n1 + 1 in Seg (n1 + 2) by A6, FINSEQ_1:1;
set f1 = R | (n1 + 1);
set s = R . (n1 + 2);
set r = R . (n1 + 1);
A9: n1 + 2 = len R by A4;
A10: len (R | (n1 + 1)) = n1 + 1 by A4, FINSEQ_1:59, NAT_1:11;
thus Sum (MIM R) = Sum (((MIM R) | n1) ^ <*((R . (n1 + 1)) - (R . (n1 + 2))),(R . (n1 + 2))*>) by A4, Th11
.= (Sum ((MIM R) | n1)) + (Sum <*((R . (n1 + 1)) - (R . (n1 + 2))),(R . (n1 + 2))*>) by RVSUM_1:75
.= (Sum ((MIM R) | n1)) + (((R . (n1 + 1)) - (R . (n1 + 2))) + (R . (n1 + 2))) by RVSUM_1:77
.= Sum (((MIM R) | n1) ^ <*(R . (n1 + 1))*>) by RVSUM_1:74
.= Sum (MIM (R | (n1 + 1))) by A9, Th10
.= (R | (n1 + 1)) . 1 by A3, A10
.= R . 1 by A4, A8, A7, Th6 ; ::_thesis: verum
end;
end;
end;
hence Sum (MIM R) = R . 1 ; ::_thesis: verum
end;
A11: S2[ 0 ] ;
for n being Element of NAT holds S2[n] from NAT_1:sch_1(A11, A2);
hence Sum (MIM R) = R . 1 by A1; ::_thesis: verum
end;
theorem :: RFINSEQ:17
for R being FinSequence of REAL
for n being Element of NAT st n < len R holds
Sum (MIM (R /^ n)) = R . (n + 1)
proof
let R be FinSequence of REAL ; ::_thesis: for n being Element of NAT st n < len R holds
Sum (MIM (R /^ n)) = R . (n + 1)
let n be Element of NAT ; ::_thesis: ( n < len R implies Sum (MIM (R /^ n)) = R . (n + 1) )
assume A1: n < len R ; ::_thesis: Sum (MIM (R /^ n)) = R . (n + 1)
then A2: len (R /^ n) = (len R) - n by Def1;
n + 1 <= len R by A1, NAT_1:13;
then 1 <= (len R) - n by XREAL_1:19;
then A3: 1 in dom (R /^ n) by A2, FINSEQ_3:25;
len (R /^ n) <> 0 by A1, A2;
hence Sum (MIM (R /^ n)) = (R /^ n) . 1 by Th16
.= R . (n + 1) by A1, A3, Def1 ;
::_thesis: verum
end;
definition
let IT be FinSequence of REAL ;
redefine attr IT is non-increasing means :Def3: :: RFINSEQ:def 3
for n being Element of NAT st n in dom IT & n + 1 in dom IT holds
IT . n >= IT . (n + 1);
compatibility
( IT is non-increasing iff for n being Element of NAT st n in dom IT & n + 1 in dom IT holds
IT . n >= IT . (n + 1) )
proof
thus ( IT is non-increasing implies for n being Element of NAT st n in dom IT & n + 1 in dom IT holds
IT . n >= IT . (n + 1) ) ::_thesis: ( ( for n being Element of NAT st n in dom IT & n + 1 in dom IT holds
IT . n >= IT . (n + 1) ) implies IT is non-increasing )
proof
assume A1: IT is non-increasing ; ::_thesis: for n being Element of NAT st n in dom IT & n + 1 in dom IT holds
IT . n >= IT . (n + 1)
let n be Element of NAT ; ::_thesis: ( n in dom IT & n + 1 in dom IT implies IT . n >= IT . (n + 1) )
assume A2: ( n in dom IT & n + 1 in dom IT ) ; ::_thesis: IT . n >= IT . (n + 1)
n + 0 <= n + 1 by XREAL_1:6;
hence IT . n >= IT . (n + 1) by A1, A2, SEQM_3:def_4; ::_thesis: verum
end;
assume A3: for n being Element of NAT st n in dom IT & n + 1 in dom IT holds
IT . n >= IT . (n + 1) ; ::_thesis: IT is non-increasing
let m be Element of NAT ; :: according to SEQM_3:def_4 ::_thesis: for b1 being Element of NAT holds
( not m in dom IT or not b1 in dom IT or not m <= b1 or IT . b1 <= IT . m )
let n be Element of NAT ; ::_thesis: ( not m in dom IT or not n in dom IT or not m <= n or IT . n <= IT . m )
assume that
A4: m in dom IT and
A5: ( n in dom IT & m <= n ) ; ::_thesis: IT . n <= IT . m
defpred S2[ Nat] means ( $1 in dom IT & m <= $1 implies IT . m >= IT . $1 );
A6: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] )
assume that
A7: S2[k] and
A8: k + 1 in dom IT ; ::_thesis: ( not m <= k + 1 or IT . m >= IT . (k + 1) )
assume m <= k + 1 ; ::_thesis: IT . m >= IT . (k + 1)
then A9: ( m < k + 1 or m = k + 1 ) by XXREAL_0:1;
percases ( m <= k or m = k + 1 ) by A9, NAT_1:13;
supposeA10: m <= k ; ::_thesis: IT . m >= IT . (k + 1)
( k + 0 <= k + 1 & k + 1 <= len IT ) by A8, FINSEQ_3:25, XREAL_1:6;
then A11: k <= len IT by XXREAL_0:2;
1 <= m by A4, FINSEQ_3:25;
then A12: 1 <= k by A10, XXREAL_0:2;
then k in dom IT by A11, FINSEQ_3:25;
then IT . k >= IT . (k + 1) by A3, A8;
hence IT . m >= IT . (k + 1) by A7, A10, A12, A11, FINSEQ_3:25, XXREAL_0:2; ::_thesis: verum
end;
suppose m = k + 1 ; ::_thesis: IT . m >= IT . (k + 1)
hence IT . m >= IT . (k + 1) ; ::_thesis: verum
end;
end;
end;
A13: S2[ 0 ] by FINSEQ_3:24;
for k being Element of NAT holds S2[k] from NAT_1:sch_1(A13, A6);
hence IT . n <= IT . m by A5; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines non-increasing RFINSEQ:def_3_:_
for IT being FinSequence of REAL holds
( IT is non-increasing iff for n being Element of NAT st n in dom IT & n + 1 in dom IT holds
IT . n >= IT . (n + 1) );
registration
cluster Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V51() V52() V53() non-increasing for FinSequence of REAL ;
existence
ex b1 being FinSequence of REAL st b1 is non-increasing
proof
take <*> REAL ; ::_thesis: <*> REAL is non-increasing
let n be Element of NAT ; :: according to RFINSEQ:def_3 ::_thesis: ( n in dom (<*> REAL) & n + 1 in dom (<*> REAL) implies (<*> REAL) . n >= (<*> REAL) . (n + 1) )
thus ( n in dom (<*> REAL) & n + 1 in dom (<*> REAL) implies (<*> REAL) . n >= (<*> REAL) . (n + 1) ) ; ::_thesis: verum
end;
end;
theorem Th18: :: RFINSEQ:18
for R being FinSequence of REAL st ( len R = 0 or len R = 1 ) holds
R is non-increasing
proof
let R be FinSequence of REAL ; ::_thesis: ( ( len R = 0 or len R = 1 ) implies R is non-increasing )
assume A1: ( len R = 0 or len R = 1 ) ; ::_thesis: R is non-increasing
now__::_thesis:_(_(_len_R_=_0_&_R_is_non-increasing_)_or_(_len_R_=_1_&_R_is_non-increasing_)_)
percases ( len R = 0 or len R = 1 ) by A1;
case len R = 0 ; ::_thesis: R is non-increasing
then R = <*> REAL ;
then for n being Element of NAT st n in dom R & n + 1 in dom R holds
R . n >= R . (n + 1) ;
hence R is non-increasing by Def3; ::_thesis: verum
end;
case len R = 1 ; ::_thesis: R is non-increasing
then A2: dom R = {1} by FINSEQ_1:2, FINSEQ_1:def_3;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_R_&_n_+_1_in_dom_R_holds_
R_._n_>=_R_._(n_+_1)
let n be Element of NAT ; ::_thesis: ( n in dom R & n + 1 in dom R implies R . n >= R . (n + 1) )
assume that
A3: n in dom R and
A4: n + 1 in dom R ; ::_thesis: R . n >= R . (n + 1)
n = 1 by A2, A3, TARSKI:def_1;
hence R . n >= R . (n + 1) by A2, A4, TARSKI:def_1; ::_thesis: verum
end;
hence R is non-increasing by Def3; ::_thesis: verum
end;
end;
end;
hence R is non-increasing ; ::_thesis: verum
end;
theorem Th19: :: RFINSEQ:19
for R being FinSequence of REAL holds
( R is non-increasing iff for n, m being Element of NAT st n in dom R & m in dom R & n < m holds
R . n >= R . m )
proof
let R be FinSequence of REAL ; ::_thesis: ( R is non-increasing iff for n, m being Element of NAT st n in dom R & m in dom R & n < m holds
R . n >= R . m )
thus ( R is non-increasing implies for n, m being Element of NAT st n in dom R & m in dom R & n < m holds
R . n >= R . m ) ::_thesis: ( ( for n, m being Element of NAT st n in dom R & m in dom R & n < m holds
R . n >= R . m ) implies R is non-increasing )
proof
defpred S2[ Nat] means ( $1 in dom R implies for n being Element of NAT st n in dom R & n < $1 holds
R . n >= R . $1 );
assume A1: R is non-increasing ; ::_thesis: for n, m being Element of NAT st n in dom R & m in dom R & n < m holds
R . n >= R . m
A2: for m being Element of NAT st S2[m] holds
S2[m + 1]
proof
let m be Element of NAT ; ::_thesis: ( S2[m] implies S2[m + 1] )
assume A3: S2[m] ; ::_thesis: S2[m + 1]
assume A4: m + 1 in dom R ; ::_thesis: for n being Element of NAT st n in dom R & n < m + 1 holds
R . n >= R . (m + 1)
then m + 1 <= len R by FINSEQ_3:25;
then A5: m <= len R by NAT_1:13;
let n be Element of NAT ; ::_thesis: ( n in dom R & n < m + 1 implies R . n >= R . (m + 1) )
assume that
A6: n in dom R and
A7: n < m + 1 ; ::_thesis: R . n >= R . (m + 1)
set t = R . m;
set r = R . n;
set s = R . (m + 1);
A8: n <= m by A7, NAT_1:13;
1 <= n by A6, FINSEQ_3:25;
then A9: 1 <= m by A8, XXREAL_0:2;
then A10: m in dom R by A5, FINSEQ_3:25;
now__::_thesis:_(_(_n_=_m_&_R_._n_>=_R_._(m_+_1)_)_or_(_n_<>_m_&_R_._n_>=_R_._(m_+_1)_)_)
percases ( n = m or n <> m ) ;
case n = m ; ::_thesis: R . n >= R . (m + 1)
hence R . n >= R . (m + 1) by A1, A4, A6, Def3; ::_thesis: verum
end;
case n <> m ; ::_thesis: R . n >= R . (m + 1)
then n < m by A8, XXREAL_0:1;
then A11: R . n >= R . m by A3, A6, A9, A5, FINSEQ_3:25;
R . m >= R . (m + 1) by A1, A4, A10, Def3;
hence R . n >= R . (m + 1) by A11, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence R . n >= R . (m + 1) ; ::_thesis: verum
end;
Seg (len R) = dom R by FINSEQ_1:def_3;
then A12: S2[ 0 ] by FINSEQ_1:1;
for m being Element of NAT holds S2[m] from NAT_1:sch_1(A12, A2);
hence for n, m being Element of NAT st n in dom R & m in dom R & n < m holds
R . n >= R . m ; ::_thesis: verum
end;
assume A13: for n, m being Element of NAT st n in dom R & m in dom R & n < m holds
R . n >= R . m ; ::_thesis: R is non-increasing
let n be Element of NAT ; :: according to RFINSEQ:def_3 ::_thesis: ( n in dom R & n + 1 in dom R implies R . n >= R . (n + 1) )
A14: n < n + 1 by NAT_1:13;
assume ( n in dom R & n + 1 in dom R ) ; ::_thesis: R . n >= R . (n + 1)
hence R . n >= R . (n + 1) by A13, A14; ::_thesis: verum
end;
theorem Th20: :: RFINSEQ:20
for R being non-increasing FinSequence of REAL
for n being Element of NAT holds R | n is non-increasing FinSequence of REAL
proof
let f be non-increasing FinSequence of REAL ; ::_thesis: for n being Element of NAT holds f | n is non-increasing FinSequence of REAL
let n be Element of NAT ; ::_thesis: f | n is non-increasing FinSequence of REAL
set fn = f | n;
now__::_thesis:_(_(_n_=_0_&_f_|_n_is_non-increasing_FinSequence_of_REAL_)_or_(_n_<>_0_&_f_|_n_is_non-increasing_FinSequence_of_REAL_)_)
percases ( n = 0 or n <> 0 ) ;
case n = 0 ; ::_thesis: f | n is non-increasing FinSequence of REAL
then len (f | n) = 0 ;
hence f | n is non-increasing FinSequence of REAL by Th18; ::_thesis: verum
end;
case n <> 0 ; ::_thesis: f | n is non-increasing FinSequence of REAL
then 0 < n by NAT_1:3;
then A1: 0 + 1 <= n by NAT_1:13;
now__::_thesis:_(_(_len_f_<=_n_&_f_|_n_is_non-increasing_FinSequence_of_REAL_)_or_(_n_<_len_f_&_f_|_n_is_non-increasing_FinSequence_of_REAL_)_)
percases ( len f <= n or n < len f ) ;
case len f <= n ; ::_thesis: f | n is non-increasing FinSequence of REAL
hence f | n is non-increasing FinSequence of REAL by Lm3; ::_thesis: verum
end;
case n < len f ; ::_thesis: f | n is non-increasing FinSequence of REAL
then A2: ( n in dom f & len (f | n) = n ) by A1, FINSEQ_1:59, FINSEQ_3:25;
now__::_thesis:_for_m_being_Element_of_NAT_st_m_in_dom_(f_|_n)_&_m_+_1_in_dom_(f_|_n)_holds_
(f_|_n)_._m_>=_(f_|_n)_._(m_+_1)
let m be Element of NAT ; ::_thesis: ( m in dom (f | n) & m + 1 in dom (f | n) implies (f | n) . m >= (f | n) . (m + 1) )
A3: dom (f | n) = Seg (len (f | n)) by FINSEQ_1:def_3;
assume A4: ( m in dom (f | n) & m + 1 in dom (f | n) ) ; ::_thesis: (f | n) . m >= (f | n) . (m + 1)
then A5: ( m in dom f & m + 1 in dom f ) by A2, A3, Th6;
( f . m = (f | n) . m & f . (m + 1) = (f | n) . (m + 1) ) by A2, A4, A3, Th6;
hence (f | n) . m >= (f | n) . (m + 1) by A5, Def3; ::_thesis: verum
end;
hence f | n is non-increasing FinSequence of REAL by Def3; ::_thesis: verum
end;
end;
end;
hence f | n is non-increasing FinSequence of REAL ; ::_thesis: verum
end;
end;
end;
hence f | n is non-increasing FinSequence of REAL ; ::_thesis: verum
end;
theorem :: RFINSEQ:21
for R being non-increasing FinSequence of REAL
for n being Element of NAT holds R /^ n is non-increasing
proof
let f be non-increasing FinSequence of REAL ; ::_thesis: for n being Element of NAT holds f /^ n is non-increasing
let n be Element of NAT ; ::_thesis: f /^ n is non-increasing
set fn = f /^ n;
now__::_thesis:_for_m_being_Element_of_NAT_st_m_in_dom_(f_/^_n)_&_m_+_1_in_dom_(f_/^_n)_holds_
(f_/^_n)_._m_>=_(f_/^_n)_._(m_+_1)
let m be Element of NAT ; ::_thesis: ( m in dom (f /^ n) & m + 1 in dom (f /^ n) implies (f /^ n) . m >= (f /^ n) . (m + 1) )
assume that
A1: m in dom (f /^ n) and
A2: m + 1 in dom (f /^ n) ; ::_thesis: (f /^ n) . m >= (f /^ n) . (m + 1)
A3: m <= m + n by NAT_1:11;
1 <= m by A1, FINSEQ_3:25;
then A4: 1 <= m + n by A3, XXREAL_0:2;
A5: 1 <= (m + n) + 1 by NAT_1:11;
A6: m + 1 <= len (f /^ n) by A2, FINSEQ_3:25;
set r = (f /^ n) . m;
set s = (f /^ n) . (m + 1);
A7: (m + 1) + n = (m + n) + 1 ;
A8: m <= len (f /^ n) by A1, FINSEQ_3:25;
now__::_thesis:_(_(_n_<=_len_f_&_(f_/^_n)_._m_>=_(f_/^_n)_._(m_+_1)_)_or_(_len_f_<_n_&_(f_/^_n)_._m_>=_(f_/^_n)_._(m_+_1)_)_)
percases ( n <= len f or len f < n ) ;
caseA9: n <= len f ; ::_thesis: (f /^ n) . m >= (f /^ n) . (m + 1)
then A10: len (f /^ n) = (len f) - n by Def1;
then m + n <= len f by A8, XREAL_1:19;
then A11: m + n in dom f by A4, FINSEQ_3:25;
(m + n) + 1 <= len f by A6, A7, A10, XREAL_1:19;
then A12: (m + n) + 1 in dom f by A5, FINSEQ_3:25;
( (f /^ n) . m = f . (m + n) & (f /^ n) . (m + 1) = f . ((m + n) + 1) ) by A1, A2, A7, A9, Def1;
hence (f /^ n) . m >= (f /^ n) . (m + 1) by A11, A12, Def3; ::_thesis: verum
end;
case len f < n ; ::_thesis: (f /^ n) . m >= (f /^ n) . (m + 1)
then f /^ n = <*> REAL by Def1;
hence (f /^ n) . m >= (f /^ n) . (m + 1) ; ::_thesis: verum
end;
end;
end;
hence (f /^ n) . m >= (f /^ n) . (m + 1) ; ::_thesis: verum
end;
hence f /^ n is non-increasing by Def3; ::_thesis: verum
end;
Lm4: for f, g being non-increasing FinSequence of REAL
for n being Element of NAT st len f = n + 1 & len f = len g & f,g are_fiberwise_equipotent holds
( f . (len f) = g . (len g) & f | n,g | n are_fiberwise_equipotent )
proof
let f, g be non-increasing FinSequence of REAL ; ::_thesis: for n being Element of NAT st len f = n + 1 & len f = len g & f,g are_fiberwise_equipotent holds
( f . (len f) = g . (len g) & f | n,g | n are_fiberwise_equipotent )
let n be Element of NAT ; ::_thesis: ( len f = n + 1 & len f = len g & f,g are_fiberwise_equipotent implies ( f . (len f) = g . (len g) & f | n,g | n are_fiberwise_equipotent ) )
assume that
A1: len f = n + 1 and
A2: len f = len g and
A3: f,g are_fiberwise_equipotent ; ::_thesis: ( f . (len f) = g . (len g) & f | n,g | n are_fiberwise_equipotent )
set r = f . (n + 1);
set s = g . (n + 1);
0 < n + 1 by NAT_1:3;
then A4: 0 + 1 <= n + 1 by NAT_1:13;
then A5: n + 1 in dom f by A1, FINSEQ_3:25;
A6: f = (f | n) ^ <*(f . (n + 1))*> by A1, Th7;
A7: n + 1 in dom g by A1, A2, A4, FINSEQ_3:25;
A8: now__::_thesis:_not_f_._(n_+_1)_<>_g_._(n_+_1)
A9: rng f = rng g by A3, CLASSES1:75;
assume A10: f . (n + 1) <> g . (n + 1) ; ::_thesis: contradiction
now__::_thesis:_(_(_f_._(n_+_1)_>_g_._(n_+_1)_&_contradiction_)_or_(_f_._(n_+_1)_<_g_._(n_+_1)_&_contradiction_)_)
percases ( f . (n + 1) > g . (n + 1) or f . (n + 1) < g . (n + 1) ) by A10, XXREAL_0:1;
caseA11: f . (n + 1) > g . (n + 1) ; ::_thesis: contradiction
g . (n + 1) in rng f by A7, A9, FUNCT_1:def_3;
then consider m being Nat such that
A12: m in dom f and
A13: f . m = g . (n + 1) by FINSEQ_2:10;
A14: m <= len f by A12, FINSEQ_3:25;
now__::_thesis:_(_(_m_=_len_f_&_contradiction_)_or_(_m_<>_len_f_&_contradiction_)_)
percases ( m = len f or m <> len f ) ;
case m = len f ; ::_thesis: contradiction
hence contradiction by A1, A11, A13; ::_thesis: verum
end;
case m <> len f ; ::_thesis: contradiction
then m < n + 1 by A1, A14, XXREAL_0:1;
hence contradiction by A5, A11, A12, A13, Th19; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
caseA15: f . (n + 1) < g . (n + 1) ; ::_thesis: contradiction
f . (n + 1) in rng g by A5, A9, FUNCT_1:def_3;
then consider m being Nat such that
A16: m in dom g and
A17: g . m = f . (n + 1) by FINSEQ_2:10;
A18: m <= len g by A16, FINSEQ_3:25;
now__::_thesis:_(_(_m_=_len_g_&_contradiction_)_or_(_m_<>_len_g_&_contradiction_)_)
percases ( m = len g or m <> len g ) ;
case m = len g ; ::_thesis: contradiction
hence contradiction by A1, A2, A15, A17; ::_thesis: verum
end;
case m <> len g ; ::_thesis: contradiction
then m < n + 1 by A1, A2, A18, XXREAL_0:1;
hence contradiction by A7, A15, A16, A17, Th19; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
hence f . (len f) = g . (len g) by A1, A2; ::_thesis: f | n,g | n are_fiberwise_equipotent
A19: g = (g | n) ^ <*(f . (n + 1))*> by A1, A2, A8, Th7;
now__::_thesis:_for_x_being_set_holds_card_(Coim_((f_|_n),x))_=_card_(Coim_((g_|_n),x))
let x be set ; ::_thesis: card (Coim ((f | n),x)) = card (Coim ((g | n),x))
(card (Coim ((f | n),x))) + (card (<*(f . (n + 1))*> " {x})) = card (Coim (f,x)) by A6, FINSEQ_3:57
.= card (Coim (g,x)) by A3, CLASSES1:def_9
.= (card (Coim ((g | n),x))) + (card (<*(f . (n + 1))*> " {x})) by A19, FINSEQ_3:57 ;
hence card (Coim ((f | n),x)) = card (Coim ((g | n),x)) ; ::_thesis: verum
end;
hence f | n,g | n are_fiberwise_equipotent by CLASSES1:def_9; ::_thesis: verum
end;
defpred S2[ Nat] means for R being FinSequence of REAL st $1 = len R holds
ex b being non-increasing FinSequence of REAL st R,b are_fiberwise_equipotent ;
Lm5: S2[ 0 ]
proof
let R be FinSequence of REAL ; ::_thesis: ( 0 = len R implies ex b being non-increasing FinSequence of REAL st R,b are_fiberwise_equipotent )
assume len R = 0 ; ::_thesis: ex b being non-increasing FinSequence of REAL st R,b are_fiberwise_equipotent
then reconsider a = R as non-increasing FinSequence of REAL by Th18;
take a ; ::_thesis: R,a are_fiberwise_equipotent
thus R,a are_fiberwise_equipotent ; ::_thesis: verum
end;
Lm6: for n being Element of NAT st S2[n] holds
S2[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] )
assume A1: S2[n] ; ::_thesis: S2[n + 1]
let R be FinSequence of REAL ; ::_thesis: ( n + 1 = len R implies ex b being non-increasing FinSequence of REAL st R,b are_fiberwise_equipotent )
set fn = R | (Seg n);
A2: R | (Seg n) = R | n by FINSEQ_1:def_15;
set q = R . (n + 1);
reconsider fn = R | (Seg n) as FinSequence by FINSEQ_1:15;
rng fn c= rng R by RELAT_1:70;
then rng fn c= REAL by XBOOLE_1:1;
then reconsider fn = fn as FinSequence of REAL by FINSEQ_1:def_4;
n <= n + 1 by NAT_1:11;
then A3: ( dom fn = (dom R) /\ (Seg n) & Seg n c= Seg (n + 1) ) by FINSEQ_1:5, RELAT_1:61;
assume A4: n + 1 = len R ; ::_thesis: ex b being non-increasing FinSequence of REAL st R,b are_fiberwise_equipotent
then dom R = Seg (n + 1) by FINSEQ_1:def_3;
then dom fn = Seg n by A3, XBOOLE_1:28;
then A5: len fn = n by FINSEQ_1:def_3;
then consider a being non-increasing FinSequence of REAL such that
A6: fn,a are_fiberwise_equipotent by A1;
A7: len fn = len a by A6, Th3;
A8: Seg (len a) = dom a by FINSEQ_1:def_3;
now__::_thesis:_(_(_(_for_t_being_Real_st_t_in_rng_a_holds_
R_._(n_+_1)_<=_t_)_&_ex_b_being_non-increasing_FinSequence_of_REAL_st_R,b_are_fiberwise_equipotent_)_or_(_ex_t_being_Real_st_
(_t_in_rng_a_&_not_R_._(n_+_1)_<=_t_)_&_ex_b_being_non-increasing_FinSequence_of_REAL_st_R,b_are_fiberwise_equipotent_)_)
percases ( for t being Real st t in rng a holds
R . (n + 1) <= t or ex t being Real st
( t in rng a & not R . (n + 1) <= t ) ) ;
caseA9: for t being Real st t in rng a holds
R . (n + 1) <= t ; ::_thesis: ex b being non-increasing FinSequence of REAL st R,b are_fiberwise_equipotent
set b = a ^ <*(R . (n + 1))*>;
A10: len (a ^ <*(R . (n + 1))*>) = n + (len <*(R . (n + 1))*>) by A5, A7, FINSEQ_1:22
.= n + 1 by FINSEQ_1:39 ;
now__::_thesis:_for_m_being_Element_of_NAT_st_m_in_dom_(a_^_<*(R_._(n_+_1))*>)_&_m_+_1_in_dom_(a_^_<*(R_._(n_+_1))*>)_holds_
(a_^_<*(R_._(n_+_1))*>)_._m_>=_(a_^_<*(R_._(n_+_1))*>)_._(m_+_1)
let m be Element of NAT ; ::_thesis: ( m in dom (a ^ <*(R . (n + 1))*>) & m + 1 in dom (a ^ <*(R . (n + 1))*>) implies (a ^ <*(R . (n + 1))*>) . m >= (a ^ <*(R . (n + 1))*>) . (m + 1) )
assume that
A11: m in dom (a ^ <*(R . (n + 1))*>) and
A12: m + 1 in dom (a ^ <*(R . (n + 1))*>) ; ::_thesis: (a ^ <*(R . (n + 1))*>) . m >= (a ^ <*(R . (n + 1))*>) . (m + 1)
A13: 1 <= m + 1 by A12, FINSEQ_3:25;
set r = (a ^ <*(R . (n + 1))*>) . m;
set s = (a ^ <*(R . (n + 1))*>) . (m + 1);
A14: 1 <= m by A11, FINSEQ_3:25;
A15: m + 1 <= len (a ^ <*(R . (n + 1))*>) by A12, FINSEQ_3:25;
then m <= (n + 1) - 1 by A10, XREAL_1:19;
then m in Seg n by A14, FINSEQ_1:1;
then A16: m in dom a by A5, A7, FINSEQ_1:def_3;
then A17: (a ^ <*(R . (n + 1))*>) . m = a . m by FINSEQ_1:def_7;
A18: a . m in rng a by A16, FUNCT_1:def_3;
now__::_thesis:_(_(_m_+_1_=_len_(a_^_<*(R_._(n_+_1))*>)_&_(a_^_<*(R_._(n_+_1))*>)_._m_>=_(a_^_<*(R_._(n_+_1))*>)_._(m_+_1)_)_or_(_m_+_1_<>_len_(a_^_<*(R_._(n_+_1))*>)_&_(a_^_<*(R_._(n_+_1))*>)_._m_>=_(a_^_<*(R_._(n_+_1))*>)_._(m_+_1)_)_)
percases ( m + 1 = len (a ^ <*(R . (n + 1))*>) or m + 1 <> len (a ^ <*(R . (n + 1))*>) ) ;
case m + 1 = len (a ^ <*(R . (n + 1))*>) ; ::_thesis: (a ^ <*(R . (n + 1))*>) . m >= (a ^ <*(R . (n + 1))*>) . (m + 1)
then (a ^ <*(R . (n + 1))*>) . (m + 1) = R . (n + 1) by A5, A7, A10, FINSEQ_1:42;
hence (a ^ <*(R . (n + 1))*>) . m >= (a ^ <*(R . (n + 1))*>) . (m + 1) by A9, A17, A18; ::_thesis: verum
end;
case m + 1 <> len (a ^ <*(R . (n + 1))*>) ; ::_thesis: (a ^ <*(R . (n + 1))*>) . m >= (a ^ <*(R . (n + 1))*>) . (m + 1)
then m + 1 < len (a ^ <*(R . (n + 1))*>) by A15, XXREAL_0:1;
then m + 1 <= (n + 1) - 1 by A10, NAT_1:13;
then m + 1 in Seg n by A13, FINSEQ_1:1;
then A19: m + 1 in dom a by A5, A7, FINSEQ_1:def_3;
then a . (m + 1) = (a ^ <*(R . (n + 1))*>) . (m + 1) by FINSEQ_1:def_7;
hence (a ^ <*(R . (n + 1))*>) . m >= (a ^ <*(R . (n + 1))*>) . (m + 1) by A16, A17, A19, Def3; ::_thesis: verum
end;
end;
end;
hence (a ^ <*(R . (n + 1))*>) . m >= (a ^ <*(R . (n + 1))*>) . (m + 1) ; ::_thesis: verum
end;
then reconsider b = a ^ <*(R . (n + 1))*> as non-increasing FinSequence of REAL by Def3;
take b = b; ::_thesis: R,b are_fiberwise_equipotent
fn ^ <*(R . (n + 1))*> = R by A4, A2, Th7;
hence R,b are_fiberwise_equipotent by A6, Th1; ::_thesis: verum
end;
caseA20: ex t being Real st
( t in rng a & not R . (n + 1) <= t ) ; ::_thesis: ex b being non-increasing FinSequence of REAL st R,b are_fiberwise_equipotent
defpred S3[ Nat] means ( $1 in dom a & ( for r being Real st r = a . $1 holds
r < R . (n + 1) ) );
A21: ex k being Nat st S3[k]
proof
consider t being Real such that
A22: t in rng a and
A23: t < R . (n + 1) by A20;
consider k being Nat such that
A24: k in dom a and
A25: a . k = t by A22, FINSEQ_2:10;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
take k ; ::_thesis: S3[k]
thus k in dom a by A24; ::_thesis: for r being Real st r = a . k holds
r < R . (n + 1)
let r be Real; ::_thesis: ( r = a . k implies r < R . (n + 1) )
assume r = a . k ; ::_thesis: r < R . (n + 1)
hence r < R . (n + 1) by A23, A25; ::_thesis: verum
end;
consider mi being Nat such that
A26: ( S3[mi] & ( for m being Nat st S3[m] holds
mi <= m ) ) from NAT_1:sch_5(A21);
1 <= mi by A26, FINSEQ_3:25;
then max (0,(mi - 1)) = mi - 1 by FINSEQ_2:4;
then reconsider k = mi - 1 as Element of NAT by FINSEQ_2:5;
mi < mi + 1 by NAT_1:13;
then A27: k <= mi by XREAL_1:19;
A28: mi <= len a by A26, FINSEQ_3:25;
then A29: k <= len a by A27, XXREAL_0:2;
then A30: len (a /^ k) = (len a) - k by Def1;
A31: dom ((a | k) ^ <*(R . (n + 1))*>) = Seg (len ((a | k) ^ <*(R . (n + 1))*>)) by FINSEQ_1:def_3;
A32: dom (a | k) c= dom ((a | k) ^ <*(R . (n + 1))*>) by FINSEQ_1:26;
set ak = a /^ k;
set b = ((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k);
A33: dom (a | k) = Seg (len (a | k)) by FINSEQ_1:def_3;
A34: len (a | k) = k by A28, A27, FINSEQ_1:59, XXREAL_0:2;
then A35: len ((a | k) ^ <*(R . (n + 1))*>) = k + (len <*(R . (n + 1))*>) by FINSEQ_1:22
.= k + 1 by FINSEQ_1:39 ;
then A36: len (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) = (k + 1) + (len (a /^ k)) by FINSEQ_1:22;
k + 1 <= len a by A26, FINSEQ_3:25;
then A37: 1 <= len (a /^ k) by A30, XREAL_1:19;
now__::_thesis:_for_m_being_Element_of_NAT_st_m_in_dom_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_&_m_+_1_in_dom_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_holds_
(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_._m_>=_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_._(m_+_1)
let m be Element of NAT ; ::_thesis: ( m in dom (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) & m + 1 in dom (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) implies (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) )
assume that
A38: m in dom (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) and
A39: m + 1 in dom (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) ; ::_thesis: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1)
A40: 1 <= m + 1 by A39, FINSEQ_3:25;
A41: m + 1 <= len (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) by A39, FINSEQ_3:25;
set r = (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m;
set s = (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1);
A42: 1 <= m by A38, FINSEQ_3:25;
A43: m <= len (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) by A38, FINSEQ_3:25;
now__::_thesis:_(_(_m_+_1_<=_k_&_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_._m_>=_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_._(m_+_1)_)_or_(_k_<_m_+_1_&_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_._m_>=_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_._(m_+_1)_)_)
percases ( m + 1 <= k or k < m + 1 ) ;
caseA44: m + 1 <= k ; ::_thesis: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1)
dom (a | k) c= dom ((a | k) ^ (a /^ k)) by FINSEQ_1:26;
then A45: dom (a | k) c= dom a by Th8;
A46: dom a = Seg (len a) by FINSEQ_1:def_3;
m <= k by A44, NAT_1:13;
then A47: m in Seg k by A42, FINSEQ_1:1;
1 <= k by A40, A44, XXREAL_0:2;
then A48: k in dom a by A29, A46, FINSEQ_1:1;
then A49: a . m = (a | k) . m by A47, Th6;
A50: m + 1 in Seg k by A40, A44, FINSEQ_1:1;
then A51: a . (m + 1) = (a | k) . (m + 1) by A48, Th6;
A52: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) = ((a | k) ^ <*(R . (n + 1))*>) . (m + 1) by A34, A33, A32, A50, FINSEQ_1:def_7
.= a . (m + 1) by A34, A33, A50, A51, FINSEQ_1:def_7 ;
(((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m = ((a | k) ^ <*(R . (n + 1))*>) . m by A34, A33, A32, A47, FINSEQ_1:def_7
.= a . m by A34, A33, A47, A49, FINSEQ_1:def_7 ;
hence (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) by A34, A33, A47, A50, A52, A45, Def3; ::_thesis: verum
end;
case k < m + 1 ; ::_thesis: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1)
then A53: k <= m by NAT_1:13;
now__::_thesis:_(_(_k_=_m_&_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_._m_>=_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_._(m_+_1)_)_or_(_k_<>_m_&_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_._m_>=_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_._(m_+_1)_)_)
percases ( k = m or k <> m ) ;
caseA54: k = m ; ::_thesis: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1)
then m + 1 in dom ((a | k) ^ <*(R . (n + 1))*>) by A35, A31, FINSEQ_1:4;
then A55: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) = ((a | k) ^ <*(R . (n + 1))*>) . (k + 1) by A54, FINSEQ_1:def_7
.= R . (n + 1) by A34, FINSEQ_1:42 ;
A56: m in Seg k by A42, A54, FINSEQ_1:1;
A57: k in dom a by A8, A29, A42, A54, FINSEQ_1:1;
then A58: a . m = (a | k) . m by A56, Th6;
A59: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m = ((a | k) ^ <*(R . (n + 1))*>) . m by A34, A33, A32, A56, FINSEQ_1:def_7
.= a . m by A34, A33, A56, A58, FINSEQ_1:def_7 ;
now__::_thesis:_not_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_._(m_+_1)_>_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_._m
assume (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) > (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m ; ::_thesis: contradiction
then for t being Real st t = a . k holds
t < R . (n + 1) by A54, A59, A55;
then mi <= k by A26, A57;
hence contradiction by XREAL_1:44; ::_thesis: verum
end;
hence (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) ; ::_thesis: verum
end;
case k <> m ; ::_thesis: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1)
then k < m by A53, XXREAL_0:1;
then A60: k + 1 <= m by NAT_1:13;
then A61: k + 1 < m + 1 by NAT_1:13;
max (0,(m - (k + 1))) = m - (k + 1) by A60, FINSEQ_2:4;
then reconsider l = m - (k + 1) as Element of NAT by FINSEQ_2:5;
A62: l + 1 = (m + 1) - (k + 1) ;
then A63: l + 1 <= (len (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k))) - (k + 1) by A41, XREAL_1:13;
l <= l + 1 by NAT_1:11;
then A64: l <= len (a /^ k) by A36, A63, XXREAL_0:2;
1 <= l + 1 by NAT_1:11;
then A65: l + 1 in dom (a /^ k) by A36, A63, FINSEQ_3:25;
1 <= (l + 1) + k by A38, FINSEQ_3:25;
then A66: (k + l) + 1 <= len a by A30, A36, A63, XREAL_1:19;
then A67: (k + l) + 1 in dom a by A42, FINSEQ_3:25;
k + l <= (k + l) + 1 by NAT_1:11;
then A68: k + l <= len a by A66, XXREAL_0:2;
A69: k + (l + 1) <= len a by A30, A36, A63, XREAL_1:19;
now__::_thesis:_(_(_k_+_1_=_m_&_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_._m_>=_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_._(m_+_1)_)_or_(_k_+_1_<>_m_&_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_._m_>=_(((a_|_k)_^_<*(R_._(n_+_1))*>)_^_(a_/^_k))_._(m_+_1)_)_)
percases ( k + 1 = m or k + 1 <> m ) ;
caseA70: k + 1 = m ; ::_thesis: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1)
then m in Seg (k + 1) by A42, FINSEQ_1:1;
then A71: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m = ((a | k) ^ <*(R . (n + 1))*>) . (k + 1) by A35, A31, A70, FINSEQ_1:def_7
.= R . (n + 1) by A34, FINSEQ_1:42 ;
A72: 1 in dom (a /^ k) by A37, FINSEQ_3:25;
(((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) = (a /^ k) . (((k + 1) + 1) - (k + 1)) by A35, A41, A61, A70, FINSEQ_1:24
.= a . mi by A29, A72, Def1 ;
hence (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) by A26, A71; ::_thesis: verum
end;
case k + 1 <> m ; ::_thesis: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1)
then A73: k + 1 < m by A60, XXREAL_0:1;
then (k + 1) + 1 <= m by NAT_1:13;
then A74: 1 <= l by XREAL_1:19;
then A75: l in dom (a /^ k) by A64, FINSEQ_3:25;
l <= k + l by NAT_1:11;
then 1 <= k + l by A74, XXREAL_0:2;
then A76: k + l in dom a by A68, FINSEQ_3:25;
A77: (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m = (a /^ k) . l by A35, A43, A73, FINSEQ_1:24
.= a . (k + l) by A29, A75, Def1 ;
(((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) = (a /^ k) . (l + 1) by A35, A41, A61, A62, FINSEQ_1:24
.= a . ((k + l) + 1) by A29, A65, A69, Def1 ;
hence (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) by A67, A77, A76, Def3; ::_thesis: verum
end;
end;
end;
hence (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) ; ::_thesis: verum
end;
end;
end;
hence (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) ; ::_thesis: verum
end;
end;
end;
hence (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . m >= (((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k)) . (m + 1) ; ::_thesis: verum
end;
then reconsider b = ((a | k) ^ <*(R . (n + 1))*>) ^ (a /^ k) as non-increasing FinSequence of REAL by Def3;
take b = b; ::_thesis: R,b are_fiberwise_equipotent
now__::_thesis:_for_x_being_set_holds_card_(Coim_(b,x))_=_card_(Coim_(R,x))
let x be set ; ::_thesis: card (Coim (b,x)) = card (Coim (R,x))
A78: card (Coim (fn,x)) = card (Coim (a,x)) by A6, CLASSES1:def_9;
thus card (Coim (b,x)) = (card (((a | k) ^ <*(R . (n + 1))*>) " {x})) + (card ((a /^ k) " {x})) by FINSEQ_3:57
.= ((card ((a | k) " {x})) + (card (<*(R . (n + 1))*> " {x}))) + (card ((a /^ k) " {x})) by FINSEQ_3:57
.= ((card ((a | k) " {x})) + (card ((a /^ k) " {x}))) + (card (<*(R . (n + 1))*> " {x}))
.= (card (((a | k) ^ (a /^ k)) " {x})) + (card (<*(R . (n + 1))*> " {x})) by FINSEQ_3:57
.= (card (fn " {x})) + (card (<*(R . (n + 1))*> " {x})) by A78, Th8
.= card ((fn ^ <*(R . (n + 1))*>) " {x}) by FINSEQ_3:57
.= card (Coim (R,x)) by A4, A2, Th7 ; ::_thesis: verum
end;
hence R,b are_fiberwise_equipotent by CLASSES1:def_9; ::_thesis: verum
end;
end;
end;
hence ex b being non-increasing FinSequence of REAL st R,b are_fiberwise_equipotent ; ::_thesis: verum
end;
theorem Th22: :: RFINSEQ:22
for R being FinSequence of REAL ex R1 being non-increasing FinSequence of REAL st R,R1 are_fiberwise_equipotent
proof
let R be FinSequence of REAL ; ::_thesis: ex R1 being non-increasing FinSequence of REAL st R,R1 are_fiberwise_equipotent
A1: len R = len R ;
for n being Element of NAT holds S2[n] from NAT_1:sch_1(Lm5, Lm6);
hence ex R1 being non-increasing FinSequence of REAL st R,R1 are_fiberwise_equipotent by A1; ::_thesis: verum
end;
Lm7: for n being Element of NAT
for g1, g2 being non-increasing FinSequence of REAL st n = len g1 & g1,g2 are_fiberwise_equipotent holds
g1 = g2
proof
defpred S3[ Nat] means for g1, g2 being non-increasing FinSequence of REAL st $1 = len g1 & g1,g2 are_fiberwise_equipotent holds
g1 = g2;
A1: for n being Element of NAT st S3[n] holds
S3[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S3[n] implies S3[n + 1] )
assume A2: S3[n] ; ::_thesis: S3[n + 1]
let g1, g2 be non-increasing FinSequence of REAL ; ::_thesis: ( n + 1 = len g1 & g1,g2 are_fiberwise_equipotent implies g1 = g2 )
set r = g1 . (n + 1);
reconsider g1n = g1 | n, g2n = g2 | n as non-increasing FinSequence of REAL by Th20;
assume that
A3: len g1 = n + 1 and
A4: g1,g2 are_fiberwise_equipotent ; ::_thesis: g1 = g2
A5: len g2 = len g1 by A4, Th3;
then A6: g1 . (len g1) = g2 . (len g2) by A3, A4, Lm4;
A7: (g1 | n) ^ <*(g1 . (n + 1))*> = g1 by A3, Th7;
len (g1 | n) = n by A3, FINSEQ_1:59, NAT_1:11;
then g1n = g2n by A2, A3, A4, A5, Lm4;
hence g1 = g2 by A3, A5, A6, A7, Th7; ::_thesis: verum
end;
A8: S3[ 0 ]
proof
let g1, g2 be non-increasing FinSequence of REAL ; ::_thesis: ( 0 = len g1 & g1,g2 are_fiberwise_equipotent implies g1 = g2 )
assume ( len g1 = 0 & g1,g2 are_fiberwise_equipotent ) ; ::_thesis: g1 = g2
then ( len g2 = len g1 & g1 = <*> REAL ) by Th3;
hence g1 = g2 ; ::_thesis: verum
end;
thus for n being Element of NAT holds S3[n] from NAT_1:sch_1(A8, A1); ::_thesis: verum
end;
theorem :: RFINSEQ:23
for R1, R2 being non-increasing FinSequence of REAL st R1,R2 are_fiberwise_equipotent holds
R1 = R2
proof
let g1, g2 be non-increasing FinSequence of REAL ; ::_thesis: ( g1,g2 are_fiberwise_equipotent implies g1 = g2 )
A1: len g1 = len g1 ;
assume g1,g2 are_fiberwise_equipotent ; ::_thesis: g1 = g2
hence g1 = g2 by A1, Lm7; ::_thesis: verum
end;
theorem :: RFINSEQ:24
for R being FinSequence of REAL
for r, s being Real st r <> 0 holds
R " {(s / r)} = (r * R) " {s}
proof
let R be FinSequence of REAL ; ::_thesis: for r, s being Real st r <> 0 holds
R " {(s / r)} = (r * R) " {s}
let r, s be Real; ::_thesis: ( r <> 0 implies R " {(s / r)} = (r * R) " {s} )
A1: ( Seg (len R) = dom R & dom (r * R) = Seg (len (r * R)) ) by FINSEQ_1:def_3;
assume A2: r <> 0 ; ::_thesis: R " {(s / r)} = (r * R) " {s}
thus R " {(s / r)} c= (r * R) " {s} :: according to XBOOLE_0:def_10 ::_thesis: (r * R) " {s} c= R " {(s / r)}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in R " {(s / r)} or x in (r * R) " {s} )
assume A3: x in R " {(s / r)} ; ::_thesis: x in (r * R) " {s}
then reconsider i = x as Element of NAT ;
R . i in {(s / r)} by A3, FUNCT_1:def_7;
then R . i = s / r by TARSKI:def_1;
then r * (R . i) = s by A2, XCMPLX_1:87;
then (r * R) . i = s by RVSUM_1:44;
then A4: (r * R) . i in {s} by TARSKI:def_1;
i in dom R by A3, FUNCT_1:def_7;
then i in dom (r * R) by A1, FINSEQ_2:33;
hence x in (r * R) " {s} by A4, FUNCT_1:def_7; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (r * R) " {s} or x in R " {(s / r)} )
assume A5: x in (r * R) " {s} ; ::_thesis: x in R " {(s / r)}
then reconsider i = x as Element of NAT ;
(r * R) . i in {s} by A5, FUNCT_1:def_7;
then (r * R) . i = s by TARSKI:def_1;
then r * (R . i) = s by RVSUM_1:44;
then R . i = s / r by A2, XCMPLX_1:89;
then A6: R . i in {(s / r)} by TARSKI:def_1;
i in dom (r * R) by A5, FUNCT_1:def_7;
then i in dom R by A1, FINSEQ_2:33;
hence x in R " {(s / r)} by A6, FUNCT_1:def_7; ::_thesis: verum
end;
theorem :: RFINSEQ:25
for R being FinSequence of REAL holds (0 * R) " {0} = dom R
proof
let R be FinSequence of REAL ; ::_thesis: (0 * R) " {0} = dom R
A1: Seg (len (0 * R)) = dom (0 * R) by FINSEQ_1:def_3;
A2: ( len (0 * R) = len R & dom R = Seg (len R) ) by FINSEQ_1:def_3, FINSEQ_2:33;
hence (0 * R) " {0} c= dom R by A1, RELAT_1:132; :: according to XBOOLE_0:def_10 ::_thesis: dom R c= (0 * R) " {0}
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom R or x in (0 * R) " {0} )
assume A3: x in dom R ; ::_thesis: x in (0 * R) " {0}
then reconsider i = x as Element of NAT ;
(0 * R) . i = 0 * (R . i) by RVSUM_1:44
.= 0 ;
then (0 * R) . i in {0} by TARSKI:def_1;
hence x in (0 * R) " {0} by A2, A1, A3, FUNCT_1:def_7; ::_thesis: verum
end;
begin
theorem :: RFINSEQ:26
for f, g being Function st rng f = rng g & f is one-to-one & g is one-to-one holds
f,g are_fiberwise_equipotent
proof
let f, g be Function; ::_thesis: ( rng f = rng g & f is one-to-one & g is one-to-one implies f,g are_fiberwise_equipotent )
assume that
A1: rng f = rng g and
A2: f is one-to-one and
A3: g is one-to-one ; ::_thesis: f,g are_fiberwise_equipotent
let x be set ; :: according to CLASSES1:def_9 ::_thesis: card (Coim (f,x)) = card (Coim (g,x))
percases ( x in rng f or not x in rng f ) ;
supposeA4: x in rng f ; ::_thesis: card (Coim (f,x)) = card (Coim (g,x))
then card (Coim (f,x)) = 1 by A2, FINSEQ_4:73;
hence card (Coim (f,x)) = card (Coim (g,x)) by A1, A3, A4, FINSEQ_4:73; ::_thesis: verum
end;
supposeA5: not x in rng f ; ::_thesis: card (Coim (f,x)) = card (Coim (g,x))
then card (f " {x}) = 0 by CARD_1:27, FUNCT_1:72;
hence card (Coim (f,x)) = card (Coim (g,x)) by A1, A5, CARD_1:27, FUNCT_1:72; ::_thesis: verum
end;
end;
end;
theorem :: RFINSEQ:27
for D being set
for f being FinSequence of D holds f /^ (len f) = {}
proof
let D be set ; ::_thesis: for f being FinSequence of D holds f /^ (len f) = {}
let f be FinSequence of D; ::_thesis: f /^ (len f) = {}
len (f /^ (len f)) = (len f) - (len f) by Def1
.= 0 ;
hence f /^ (len f) = {} ; ::_thesis: verum
end;
theorem :: RFINSEQ:28
for f, g being Function
for m, n being set st f . m = g . n & f . n = g . m & m in dom f & n in dom f & dom f = dom g & ( for k being set st k <> m & k <> n & k in dom f holds
f . k = g . k ) holds
f,g are_fiberwise_equipotent
proof
let f, g be Function; ::_thesis: for m, n being set st f . m = g . n & f . n = g . m & m in dom f & n in dom f & dom f = dom g & ( for k being set st k <> m & k <> n & k in dom f holds
f . k = g . k ) holds
f,g are_fiberwise_equipotent
let m, n be set ; ::_thesis: ( f . m = g . n & f . n = g . m & m in dom f & n in dom f & dom f = dom g & ( for k being set st k <> m & k <> n & k in dom f holds
f . k = g . k ) implies f,g are_fiberwise_equipotent )
assume that
A1: f . m = g . n and
A2: f . n = g . m and
A3: m in dom f and
A4: n in dom f and
A5: dom f = dom g and
A6: for k being set st k <> m & k <> n & k in dom f holds
f . k = g . k ; ::_thesis: f,g are_fiberwise_equipotent
set t = id (dom f);
set nm = n .--> m;
set mn = m .--> n;
set p = ((id (dom f)) +* (n .--> m)) +* (m .--> n);
A7: dom (n .--> m) = {n} by FUNCOP_1:13;
A8: dom (id (dom f)) = dom f ;
A9: rng (id (dom f)) = dom ((id (dom f)) ") by FUNCT_1:33
.= dom f by A8, FUNCT_1:45 ;
dom (m .--> n) = {m} by FUNCOP_1:13;
then A10: dom (((id (dom f)) +* (n .--> m)) +* (m .--> n)) = (dom ((id (dom f)) +* (n .--> m))) \/ {m} by FUNCT_4:def_1
.= ((dom (id (dom f))) \/ {n}) \/ {m} by A7, FUNCT_4:def_1
.= ((dom f) \/ {n}) \/ {m}
.= (dom f) \/ {m} by A4, ZFMISC_1:40
.= dom f by A3, ZFMISC_1:40 ;
A11: now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
((((id_(dom_f))_+*_(n_.-->_m))_+*_(m_.-->_n))_*_(((id_(dom_f))_+*_(n_.-->_m))_+*_(m_.-->_n)))_._x_=_x
let x be set ; ::_thesis: ( x in dom f implies ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . b1 = b1 )
assume A12: x in dom f ; ::_thesis: ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . b1 = b1
then A13: ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = (((id (dom f)) +* (n .--> m)) +* (m .--> n)) . ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) . x) by A10, FUNCT_1:13;
percases ( x = m or x <> m ) ;
supposeA14: x = m ; ::_thesis: ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . b1 = b1
hence ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = (((id (dom f)) +* (n .--> m)) +* (m .--> n)) . n by A13, FUNCT_4:89
.= x by A14, FUNCT_4:90 ;
::_thesis: verum
end;
supposeA15: x <> m ; ::_thesis: ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . b1 = b1
now__::_thesis:_((((id_(dom_f))_+*_(n_.-->_m))_+*_(m_.-->_n))_*_(((id_(dom_f))_+*_(n_.-->_m))_+*_(m_.-->_n)))_._x_=_x
percases ( x = n or x <> n ) ;
supposeA16: x = n ; ::_thesis: ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = x
hence ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = (((id (dom f)) +* (n .--> m)) +* (m .--> n)) . m by A13, FUNCT_4:90
.= x by A16, FUNCT_4:89 ;
::_thesis: verum
end;
supposeA17: x <> n ; ::_thesis: ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = x
hence ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = (((id (dom f)) +* (n .--> m)) +* (m .--> n)) . ((id (dom f)) . x) by A13, A15, FUNCT_4:91
.= (((id (dom f)) +* (n .--> m)) +* (m .--> n)) . x by A12, FUNCT_1:17
.= (id (dom f)) . x by A15, A17, FUNCT_4:91
.= x by A12, FUNCT_1:17 ;
::_thesis: verum
end;
end;
end;
hence ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = x ; ::_thesis: verum
end;
end;
end;
rng (n .--> m) = {m} by FUNCOP_1:8;
then (rng (id (dom f))) \/ (rng (n .--> m)) = dom f by A3, ZFMISC_1:40;
then A18: (rng ((id (dom f)) +* (n .--> m))) \/ (rng (m .--> n)) c= (dom f) \/ (rng (m .--> n)) by FUNCT_4:17, XBOOLE_1:9;
for z being set st z in rng ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) holds
z in rng (((id (dom f)) +* (n .--> m)) +* (m .--> n)) by FUNCT_1:14;
then A19: rng ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) c= rng (((id (dom f)) +* (n .--> m)) +* (m .--> n)) by TARSKI:def_3;
A20: rng (((id (dom f)) +* (n .--> m)) +* (m .--> n)) c= (rng ((id (dom f)) +* (n .--> m))) \/ (rng (m .--> n)) by FUNCT_4:17;
A21: rng (m .--> n) = {n} by FUNCOP_1:8;
then (dom f) \/ (rng (m .--> n)) = dom (((id (dom f)) +* (n .--> m)) +* (m .--> n)) by A4, A10, ZFMISC_1:40;
then A22: dom ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) = dom f by A10, A18, A20, RELAT_1:27, XBOOLE_1:1;
then (((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n)) = id (dom f) by A11, FUNCT_1:17;
then A23: ((id (dom f)) +* (n .--> m)) +* (m .--> n) is one-to-one by A10, FUNCT_1:31;
rng (((id (dom f)) +* (n .--> m)) +* (m .--> n)) c= (dom f) \/ (rng (m .--> n)) by A18, A20, XBOOLE_1:1;
then A24: rng (((id (dom f)) +* (n .--> m)) +* (m .--> n)) c= dom (((id (dom f)) +* (n .--> m)) +* (m .--> n)) by A4, A10, A21, ZFMISC_1:40;
then A25: dom (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) = dom f by A5, A10, RELAT_1:27;
now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
(g_*_(((id_(dom_f))_+*_(n_.-->_m))_+*_(m_.-->_n)))_._x_=_f_._x
let x be set ; ::_thesis: ( x in dom f implies (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . b1 = f . b1 )
assume A26: x in dom f ; ::_thesis: (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . b1 = f . b1
then A27: (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = g . ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) . x) by A25, FUNCT_1:12;
percases ( x = m or x <> m ) ;
suppose x = m ; ::_thesis: (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . b1 = f . b1
hence (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = f . x by A1, A27, FUNCT_4:89; ::_thesis: verum
end;
supposeA28: x <> m ; ::_thesis: (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . b1 = f . b1
now__::_thesis:_(g_*_(((id_(dom_f))_+*_(n_.-->_m))_+*_(m_.-->_n)))_._x_=_f_._x
percases ( x = n or x <> n ) ;
suppose x = n ; ::_thesis: (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = f . x
hence (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = f . x by A2, A27, FUNCT_4:90; ::_thesis: verum
end;
supposeA29: x <> n ; ::_thesis: (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = f . x
hence (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = g . ((id (dom f)) . x) by A27, A28, FUNCT_4:91
.= g . x by A26, FUNCT_1:17
.= f . x by A6, A26, A28, A29 ;
::_thesis: verum
end;
end;
end;
hence (g * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) . x = f . x ; ::_thesis: verum
end;
end;
end;
then A30: f = g * (((id (dom f)) +* (n .--> m)) +* (m .--> n)) by A25, FUNCT_1:2;
rng ((((id (dom f)) +* (n .--> m)) +* (m .--> n)) * (((id (dom f)) +* (n .--> m)) +* (m .--> n))) = dom f by A9, A22, A11, FUNCT_1:17;
then rng (((id (dom f)) +* (n .--> m)) +* (m .--> n)) = dom g by A5, A10, A24, A19, XBOOLE_0:def_10;
hence f,g are_fiberwise_equipotent by A10, A23, A30, CLASSES1:77; ::_thesis: verum
end;
theorem :: RFINSEQ:29
for D being non empty set
for f being FinSequence of D
for k being Nat holds len (f /^ k) = (len f) -' k
proof
let D be non empty set ; ::_thesis: for f being FinSequence of D
for k being Nat holds len (f /^ k) = (len f) -' k
let f be FinSequence of D; ::_thesis: for k being Nat holds len (f /^ k) = (len f) -' k
let k be Nat; ::_thesis: len (f /^ k) = (len f) -' k
percases ( k <= len f or k > len f ) ;
supposeA1: k <= len f ; ::_thesis: len (f /^ k) = (len f) -' k
then (len f) -' k = (len f) - k by XREAL_1:233;
hence len (f /^ k) = (len f) -' k by A1, Def1; ::_thesis: verum
end;
supposeA2: k > len f ; ::_thesis: len (f /^ k) = (len f) -' k
then f /^ k = <*> D by Def1;
then A3: len (f /^ k) = 0 ;
(len f) - k < 0 by A2, XREAL_1:49;
hence len (f /^ k) = (len f) -' k by A3, XREAL_0:def_2; ::_thesis: verum
end;
end;
end;
theorem Th30: :: RFINSEQ:30
for f, g being FinSequence
for x being set st x in dom g & f,g are_fiberwise_equipotent holds
ex y being set st
( y in dom g & f . x = g . y )
proof
let f, g be FinSequence; ::_thesis: for x being set st x in dom g & f,g are_fiberwise_equipotent holds
ex y being set st
( y in dom g & f . x = g . y )
let x be set ; ::_thesis: ( x in dom g & f,g are_fiberwise_equipotent implies ex y being set st
( y in dom g & f . x = g . y ) )
assume that
A1: x in dom g and
A2: f,g are_fiberwise_equipotent ; ::_thesis: ex y being set st
( y in dom g & f . x = g . y )
consider P being Permutation of (dom g) such that
A3: f = g * P by A2, Th4;
take y = P . x; ::_thesis: ( y in dom g & f . x = g . y )
thus y in dom g by A1, FUNCT_2:5; ::_thesis: f . x = g . y
thus f . x = g . y by A1, A3, FUNCT_2:15; ::_thesis: verum
end;
theorem Th31: :: RFINSEQ:31
for f, g, h being FinSequence holds
( f,g are_fiberwise_equipotent iff h ^ f,h ^ g are_fiberwise_equipotent )
proof
let f, g, h be FinSequence; ::_thesis: ( f,g are_fiberwise_equipotent iff h ^ f,h ^ g are_fiberwise_equipotent )
thus ( f,g are_fiberwise_equipotent implies h ^ f,h ^ g are_fiberwise_equipotent ) ::_thesis: ( h ^ f,h ^ g are_fiberwise_equipotent implies f,g are_fiberwise_equipotent )
proof
assume A1: f,g are_fiberwise_equipotent ; ::_thesis: h ^ f,h ^ g are_fiberwise_equipotent
now__::_thesis:_for_y_being_set_holds_card_(Coim_((h_^_f),y))_=_card_(Coim_((h_^_g),y))
let y be set ; ::_thesis: card (Coim ((h ^ f),y)) = card (Coim ((h ^ g),y))
card (Coim (f,y)) = card (Coim (g,y)) by A1, CLASSES1:def_9;
hence card (Coim ((h ^ f),y)) = (card (g " {y})) + (card (h " {y})) by FINSEQ_3:57
.= card (Coim ((h ^ g),y)) by FINSEQ_3:57 ;
::_thesis: verum
end;
hence h ^ f,h ^ g are_fiberwise_equipotent by CLASSES1:def_9; ::_thesis: verum
end;
assume A2: h ^ f,h ^ g are_fiberwise_equipotent ; ::_thesis: f,g are_fiberwise_equipotent
now__::_thesis:_for_x_being_set_holds_card_(Coim_(f,x))_=_card_(Coim_(g,x))
let x be set ; ::_thesis: card (Coim (f,x)) = card (Coim (g,x))
A3: ( card (Coim ((h ^ f),x)) = (card (Coim (f,x))) + (card (h " {x})) & card ((h ^ g) " {x}) = (card (g " {x})) + (card (h " {x})) ) by FINSEQ_3:57;
card (Coim ((h ^ f),x)) = card (Coim ((h ^ g),x)) by A2, CLASSES1:def_9;
hence card (Coim (f,x)) = card (Coim (g,x)) by A3; ::_thesis: verum
end;
hence f,g are_fiberwise_equipotent by CLASSES1:def_9; ::_thesis: verum
end;
theorem :: RFINSEQ:32
for f, g being FinSequence
for m, n, j being Element of NAT st f,g are_fiberwise_equipotent & m <= n & n <= len f & ( for i being Element of NAT st 1 <= i & i <= m holds
f . i = g . i ) & ( for i being Element of NAT st n < i & i <= len f holds
f . i = g . i ) & m < j & j <= n holds
ex k being Element of NAT st
( m < k & k <= n & f . j = g . k )
proof
let f, g be FinSequence; ::_thesis: for m, n, j being Element of NAT st f,g are_fiberwise_equipotent & m <= n & n <= len f & ( for i being Element of NAT st 1 <= i & i <= m holds
f . i = g . i ) & ( for i being Element of NAT st n < i & i <= len f holds
f . i = g . i ) & m < j & j <= n holds
ex k being Element of NAT st
( m < k & k <= n & f . j = g . k )
let m, n, j be Element of NAT ; ::_thesis: ( f,g are_fiberwise_equipotent & m <= n & n <= len f & ( for i being Element of NAT st 1 <= i & i <= m holds
f . i = g . i ) & ( for i being Element of NAT st n < i & i <= len f holds
f . i = g . i ) & m < j & j <= n implies ex k being Element of NAT st
( m < k & k <= n & f . j = g . k ) )
assume A1: f,g are_fiberwise_equipotent ; ::_thesis: ( not m <= n or not n <= len f or ex i being Element of NAT st
( 1 <= i & i <= m & not f . i = g . i ) or ex i being Element of NAT st
( n < i & i <= len f & not f . i = g . i ) or not m < j or not j <= n or ex k being Element of NAT st
( m < k & k <= n & f . j = g . k ) )
assume that
A2: m <= n and
A3: n <= len f ; ::_thesis: ( ex i being Element of NAT st
( 1 <= i & i <= m & not f . i = g . i ) or ex i being Element of NAT st
( n < i & i <= len f & not f . i = g . i ) or not m < j or not j <= n or ex k being Element of NAT st
( m < k & k <= n & f . j = g . k ) )
assume A4: for i being Element of NAT st 1 <= i & i <= m holds
f . i = g . i ; ::_thesis: ( ex i being Element of NAT st
( n < i & i <= len f & not f . i = g . i ) or not m < j or not j <= n or ex k being Element of NAT st
( m < k & k <= n & f . j = g . k ) )
reconsider m3 = (len f) - n as Element of NAT by A3, INT_1:3, XREAL_1:48;
len g = n + m3 by A1, Th3;
then consider s2, r2 being FinSequence such that
A5: len s2 = n and
A6: len r2 = m3 and
A7: g = s2 ^ r2 by FINSEQ_2:22;
A8: len f = n + m3 ;
then consider s1, r1 being FinSequence such that
A9: len s1 = n and
A10: len r1 = m3 and
A11: f = s1 ^ r1 by FINSEQ_2:22;
A12: dom r1 = Seg m3 by A10, FINSEQ_1:def_3;
assume A13: for i being Element of NAT st n < i & i <= len f holds
f . i = g . i ; ::_thesis: ( not m < j or not j <= n or ex k being Element of NAT st
( m < k & k <= n & f . j = g . k ) )
now__::_thesis:_for_i_being_Nat_st_i_in_dom_r1_holds_
r1_._i_=_r2_._i
let i be Nat; ::_thesis: ( i in dom r1 implies r1 . i = r2 . i )
reconsider a = i as Element of NAT by ORDINAL1:def_12;
A14: n < n + 1 by XREAL_1:29;
assume A15: i in dom r1 ; ::_thesis: r1 . i = r2 . i
then A16: i in dom r2 by A6, A12, FINSEQ_1:def_3;
1 <= i by A12, A15, FINSEQ_1:1;
then n + 1 <= n + i by XREAL_1:6;
then A17: n < i + n by A14, XXREAL_0:2;
i <= m3 by A12, A15, FINSEQ_1:1;
then A18: (len s1) + i <= len f by A8, A9, XREAL_1:6;
thus r1 . i = f . ((len s1) + i) by A11, A15, FINSEQ_1:def_7
.= g . ((len s2) + a) by A13, A9, A5, A17, A18
.= r2 . i by A7, A16, FINSEQ_1:def_7 ; ::_thesis: verum
end;
then r1 = r2 by A10, A6, FINSEQ_2:9;
then A19: s1,s2 are_fiberwise_equipotent by A1, A11, A7, Th1;
reconsider m2 = n - m as Element of NAT by A2, INT_1:3, XREAL_1:48;
A20: m + 1 > m by XREAL_1:29;
len s2 = m + m2 by A5;
then consider p2, q2 being FinSequence such that
A21: len p2 = m and
A22: len q2 = m2 and
A23: s2 = p2 ^ q2 by FINSEQ_2:22;
A24: Seg m = dom p2 by A21, FINSEQ_1:def_3;
len s1 = m + m2 by A9;
then consider p1, q1 being FinSequence such that
A25: len p1 = m and
A26: len q1 = m2 and
A27: s1 = p1 ^ q1 by FINSEQ_2:22;
A28: f = p1 ^ (q1 ^ r1) by A11, A27, FINSEQ_1:32;
A29: dom p1 = Seg m by A25, FINSEQ_1:def_3;
A30: g = p2 ^ (q2 ^ r2) by A7, A23, FINSEQ_1:32;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_p1_holds_
p1_._i_=_p2_._i
let i be Nat; ::_thesis: ( i in dom p1 implies p1 . i = p2 . i )
reconsider a = i as Element of NAT by ORDINAL1:def_12;
assume A31: i in dom p1 ; ::_thesis: p1 . i = p2 . i
then A32: ( 1 <= i & i <= m ) by A29, FINSEQ_1:1;
thus p1 . i = f . i by A28, A31, FINSEQ_1:def_7
.= g . a by A4, A32
.= p2 . i by A30, A24, A29, A31, FINSEQ_1:def_7 ; ::_thesis: verum
end;
then p1 = p2 by A25, A21, FINSEQ_2:9;
then A33: q1,q2 are_fiberwise_equipotent by A27, A23, A19, Th31;
assume that
A34: m < j and
A35: j <= n ; ::_thesis: ex k being Element of NAT st
( m < k & k <= n & f . j = g . k )
j - (len p1) > 0 by A34, A25, XREAL_1:50;
then reconsider x = j - (len p1) as Element of NAT by INT_1:3;
A36: x <= n - (len p1) by A35, XREAL_1:9;
A37: Seg m2 = dom q2 by A22, FINSEQ_1:def_3;
A38: 1 + 0 <= x by A34, A25, INT_1:7, XREAL_1:50;
then x in dom q2 by A25, A37, A36, FINSEQ_1:1;
then consider y being set such that
A39: y in dom q2 and
A40: q1 . x = q2 . y by A33, Th30;
reconsider y = y as Element of NAT by A39;
A41: (len p2) + y in dom s2 by A23, A39, FINSEQ_1:28;
reconsider k = (len p2) + y as Element of NAT by ORDINAL1:def_12;
take k ; ::_thesis: ( m < k & k <= n & f . j = g . k )
1 <= y by A37, A39, FINSEQ_1:1;
then k >= (len p2) + 1 by XREAL_1:6;
hence m < k by A21, A20, XXREAL_0:2; ::_thesis: ( k <= n & f . j = g . k )
y <= m2 by A37, A39, FINSEQ_1:1;
then k <= m2 + (len p2) by XREAL_1:6;
hence k <= n by A21; ::_thesis: f . j = g . k
Seg m2 = dom q1 by A26, FINSEQ_1:def_3;
then A42: x in dom q1 by A25, A38, A36, FINSEQ_1:1;
then (len p1) + x in dom s1 by A27, FINSEQ_1:28;
hence f . j = s1 . ((len p1) + x) by A11, FINSEQ_1:def_7
.= q2 . y by A27, A40, A42, FINSEQ_1:def_7
.= s2 . ((len p2) + y) by A23, A39, FINSEQ_1:def_7
.= g . k by A7, A41, FINSEQ_1:def_7 ;
::_thesis: verum
end;
theorem :: RFINSEQ:33
for t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing )
proof
let t be FinSequence of INT ; ::_thesis: ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing )
t is FinSequence of REAL by FINSEQ_3:117;
then consider u being non-increasing FinSequence of REAL such that
A1: t,u are_fiberwise_equipotent by Th22;
take u ; ::_thesis: ( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing )
thus t,u are_fiberwise_equipotent by A1; ::_thesis: ( u is FinSequence of INT & u is non-increasing )
rng t = rng u by A1, CLASSES1:75;
hence u is FinSequence of INT by FINSEQ_1:def_4; ::_thesis: u is non-increasing
thus u is non-increasing ; ::_thesis: verum
end;