let n be Element of NAT ; :: thesis: ( S1[n] implies S1[n + 1] )
assume A1:
S1[n]
; :: thesis: S1[n + 1]
let D be non empty set ; :: thesis: for F being PartFunc of D,REAL
for X, Y being set
for Z being finite set st Z = dom (F | Y) & dom (F | X) is finite & Y c= X & n + 1 = card Z & ( for d1, d2 being Element of D st d1 in dom (F | Y) & d2 in dom (F | (X \ Y)) holds
F . d1 >= F . d2 ) holds
FinS F,X = (FinS F,Y) ^ (FinS F,(X \ Y))
let F be PartFunc of D,REAL ; :: thesis: for X, Y being set
for Z being finite set st Z = dom (F | Y) & dom (F | X) is finite & Y c= X & n + 1 = card Z & ( for d1, d2 being Element of D st d1 in dom (F | Y) & d2 in dom (F | (X \ Y)) holds
F . d1 >= F . d2 ) holds
FinS F,X = (FinS F,Y) ^ (FinS F,(X \ Y))
let X, Y be set ; :: thesis: for Z being finite set st Z = dom (F | Y) & dom (F | X) is finite & Y c= X & n + 1 = card Z & ( for d1, d2 being Element of D st d1 in dom (F | Y) & d2 in dom (F | (X \ Y)) holds
F . d1 >= F . d2 ) holds
FinS F,X = (FinS F,Y) ^ (FinS F,(X \ Y))
set dx = dom (F | X);
set dxy = dom (F | (X \ Y));
set fy = FinS F,Y;
set fxy = FinS F,(X \ Y);
let dy be finite set ; :: thesis: ( dy = dom (F | Y) & dom (F | X) is finite & Y c= X & n + 1 = card dy & ( for d1, d2 being Element of D st d1 in dom (F | Y) & d2 in dom (F | (X \ Y)) holds
F . d1 >= F . d2 ) implies FinS F,X = (FinS F,Y) ^ (FinS F,(X \ Y)) )
assume A2:
( dy = dom (F | Y) & dom (F | X) is finite & Y c= X & n + 1 = card dy & ( for d1, d2 being Element of D st d1 in dom (F | Y) & d2 in dom (F | (X \ Y)) holds
F . d1 >= F . d2 ) )
; :: thesis: FinS F,X = (FinS F,Y) ^ (FinS F,(X \ Y))
A3:
( dom (F | X) = (dom F) /\ X & dy = (dom F) /\ Y & dom (F | (X \ Y)) = (dom F) /\ (X \ Y) )
by A2, RELAT_1:90;
then A4:
( dy is finite & dom (F | (X \ Y)) is finite )
by A2, FINSET_1:13, XBOOLE_1:26;
then A5:
( F | Y, FinS F,Y are_fiberwise_equipotent & F | (X \ Y), FinS F,(X \ Y) are_fiberwise_equipotent )
by A2, Def14;
then A6:
( rng (FinS F,Y) = rng (F | Y) & rng (FinS F,(X \ Y)) = rng (F | (X \ Y)) )
by CLASSES1:83;
1 <= n + 1
then A7:
( len (FinS F,Y) = n + 1 & 1 <= n + 1 )
by A2, Th70;
then A8:
len (FinS F,Y) in dom (FinS F,Y)
by FINSEQ_3:27;
then
(FinS F,Y) . (len (FinS F,Y)) in rng (FinS F,Y)
by FUNCT_1:def 5;
then consider d being Element of D such that
A9:
( d in dy & (F | Y) . d = (FinS F,Y) . (len (FinS F,Y)) )
by A2, A6, PARTFUN1:26;
A10:
F . d = (FinS F,Y) . (len (FinS F,Y))
by A2, A9, FUNCT_1:70;
set Yd = Y \ {d};
set dyd = dom (F | (Y \ {d}));
set xyd = dom (F | (X \ (Y \ {d})));
A11:
( {d} c= dy & dom (F | (Y \ {d})) = (dom F) /\ (Y \ {d}) & dom (F | (X \ (Y \ {d}))) = (dom F) /\ (X \ (Y \ {d})) & d in Y & d in dom F )
by A3, A9, RELAT_1:90, XBOOLE_0:def 4, ZFMISC_1:37;
A12:
dom (F | (Y \ {d})) = dy \ {d}
then reconsider dyd = dom (F | (Y \ {d})) as finite set ;
A18: card dyd =
(card dy) - (card {d})
by A11, A12, CARD_2:63
.=
(n + 1) - 1
by A2, CARD_1:50
.=
n
;
A20:
( {d} c= X & {d} c= Y & {d} c= dom F )
by A2, A11, ZFMISC_1:37;
A21: X \ (Y \ {d}) =
(X \ Y) \/ (X /\ {d})
by XBOOLE_1:52
.=
(X \ Y) \/ {d}
by A20, XBOOLE_1:28
;
then A22: dom (F | (X \ (Y \ {d}))) =
(dom (F | (X \ Y))) \/ ((dom F) /\ {d})
by A3, A11, XBOOLE_1:23
.=
(dom (F | (X \ Y))) \/ {d}
by A20, XBOOLE_1:28
;
now let d1,
d2 be
Element of
D;
:: thesis: ( d1 in dyd & d2 in dom (F | (X \ (Y \ {d}))) implies F . d1 >= F . d2 )assume A23:
(
d1 in dyd &
d2 in dom (F | (X \ (Y \ {d}))) )
;
:: thesis: F . d1 >= F . d2then A24:
(
d1 in dy & not
d1 in {d} )
by A12, XBOOLE_0:def 5;
now per cases
( d2 in dom (F | (X \ Y)) or d2 in {d} )
by A22, A23, XBOOLE_0:def 3;
case
d2 in {d}
;
:: thesis: F . d1 >= F . d2then A25:
(
d2 = d &
d1 <> d )
by A24, TARSKI:def 1;
(F | Y) . d1 in rng (F | Y)
by A2, A12, A23, FUNCT_1:def 5;
then
F . d1 in rng (F | Y)
by A2, A12, A23, FUNCT_1:70;
then consider m being
Nat such that A26:
(
m in dom (FinS F,Y) &
(FinS F,Y) . m = F . d1 )
by A6, FINSEQ_2:11;
A27:
( 1
<= m &
m <= len (FinS F,Y) )
by A26, FINSEQ_3:27;
hence
F . d1 >= F . d2
;
:: thesis: verum end; hence
F . d1 >= F . d2
;
:: thesis: verum end;
then A28:
FinS F,X = (FinS F,(Y \ {d})) ^ (FinS F,(X \ (Y \ {d})))
by A1, A2, A18, XBOOLE_1:1;
A29: (X \ (Y \ {d})) \ {d} =
X \ ((Y \ {d}) \/ {d})
by XBOOLE_1:41
.=
X \ (Y \/ {d})
by XBOOLE_1:39
.=
X \ Y
by A20, XBOOLE_1:12
;
A30:
dom (F | (X \ (Y \ {d}))) is finite
by A4, A22;
d in {d}
by TARSKI:def 1;
then
d in X \ (Y \ {d})
by A21, XBOOLE_0:def 3;
then
d in dom (F | (X \ (Y \ {d})))
by A11, XBOOLE_0:def 4;
then A31:
(FinS F,(X \ Y)) ^ <*(F . d)*>,F | (X \ (Y \ {d})) are_fiberwise_equipotent
by A29, A30, Th69;
(FinS F,(X \ Y)) ^ <*(F . d)*>,<*(F . d)*> ^ (FinS F,(X \ Y)) are_fiberwise_equipotent
by RFINSEQ:15;
then A32:
<*(F . d)*> ^ (FinS F,(X \ Y)),F | (X \ (Y \ {d})) are_fiberwise_equipotent
by A31, CLASSES1:84;
<*(F . d)*> ^ (FinS F,(X \ Y)) is non-increasing
proof
let n be
Element of
NAT ;
:: according to RFINSEQ:def 4 :: thesis: ( not n in dom (<*(F . d)*> ^ (FinS F,(X \ Y))) or not n + 1 in dom (<*(F . d)*> ^ (FinS F,(X \ Y))) or (<*(F . d)*> ^ (FinS F,(X \ Y))) . (n + 1) <= (<*(F . d)*> ^ (FinS F,(X \ Y))) . n )
assume A33:
(
n in dom (<*(F . d)*> ^ (FinS F,(X \ Y))) &
n + 1
in dom (<*(F . d)*> ^ (FinS F,(X \ Y))) )
;
:: thesis: (<*(F . d)*> ^ (FinS F,(X \ Y))) . (n + 1) <= (<*(F . d)*> ^ (FinS F,(X \ Y))) . n
set xfy =
<*(F . d)*> ^ (FinS F,(X \ Y));
set r =
(<*(F . d)*> ^ (FinS F,(X \ Y))) . n;
set s =
(<*(F . d)*> ^ (FinS F,(X \ Y))) . (n + 1);
A34:
(
len <*(F . d)*> = 1 &
<*(F . d)*> . 1
= F . d )
by FINSEQ_1:57;
A35:
( 1
<= n &
n <= len (<*(F . d)*> ^ (FinS F,(X \ Y))) & 1
<= n + 1 &
n + 1
<= len (<*(F . d)*> ^ (FinS F,(X \ Y))) )
by A33, FINSEQ_3:27;
then
max 0 ,
(n - 1) = n - 1
by FINSEQ_2:4;
then reconsider n1 =
n - 1 as
Element of
NAT by FINSEQ_2:5;
len (<*(F . d)*> ^ (FinS F,(X \ Y))) = 1
+ (len (FinS F,(X \ Y)))
by A34, FINSEQ_1:35;
then A36:
len (FinS F,(X \ Y)) = (len (<*(F . d)*> ^ (FinS F,(X \ Y)))) - 1
;
then A37:
n1 <= len (FinS F,(X \ Y))
by A35, XREAL_1:11;
(
n1 + 1
<= len (FinS F,(X \ Y)) &
n < n + 1 )
by A35, A36, NAT_1:13, XREAL_1:21;
then A38:
(
n1 + 1
in dom (FinS F,(X \ Y)) & 1
< n + 1 )
by A35, FINSEQ_3:27, XXREAL_0:2;
then A39:
(<*(F . d)*> ^ (FinS F,(X \ Y))) . (n + 1) =
(FinS F,(X \ Y)) . ((n + 1) - 1)
by A34, A35, FINSEQ_1:37
.=
(FinS F,(X \ Y)) . (n1 + 1)
;
(FinS F,(X \ Y)) . (n1 + 1) in rng (FinS F,(X \ Y))
by A38, FUNCT_1:def 5;
then consider d1 being
Element of
D such that A40:
(
d1 in dom (F | (X \ Y)) &
(F | (X \ Y)) . d1 = (FinS F,(X \ Y)) . (n1 + 1) )
by A6, PARTFUN1:26;
A41:
F . d1 = (FinS F,(X \ Y)) . (n1 + 1)
by A40, FUNCT_1:70;
A42:
F . d >= F . d1
by A2, A9, A40;
now per cases
( n = 1 or n <> 1 )
;
suppose
n <> 1
;
:: thesis: (<*(F . d)*> ^ (FinS F,(X \ Y))) . n >= (<*(F . d)*> ^ (FinS F,(X \ Y))) . (n + 1)then A43:
1
< n
by A35, XXREAL_0:1;
then A44:
(<*(F . d)*> ^ (FinS F,(X \ Y))) . n = (FinS F,(X \ Y)) . n1
by A34, A35, FINSEQ_1:37;
1
+ 1
<= n
by A43, NAT_1:13;
then
1
<= n1
by XREAL_1:21;
then
n1 in dom (FinS F,(X \ Y))
by A37, FINSEQ_3:27;
hence
(<*(F . d)*> ^ (FinS F,(X \ Y))) . n >= (<*(F . d)*> ^ (FinS F,(X \ Y))) . (n + 1)
by A38, A39, A44, RFINSEQ:def 4;
:: thesis: verum end;
hence
(<*(F . d)*> ^ (FinS F,(X \ Y))) . n >= (<*(F . d)*> ^ (FinS F,(X \ Y))) . (n + 1)
;
:: thesis: verum
end;
then
<*(F . d)*> ^ (FinS F,(X \ Y)) = FinS F,(X \ (Y \ {d}))
by A30, A32, Def14;
then A45:
FinS F,X = ((FinS F,(Y \ {d})) ^ <*(F . d)*>) ^ (FinS F,(X \ Y))
by A28, FINSEQ_1:45;
F | Y,(FinS F,(Y \ {d})) ^ <*(F . d)*> are_fiberwise_equipotent
by A2, A9, Th69;
then A46:
(FinS F,(Y \ {d})) ^ <*(F . d)*>, FinS F,Y are_fiberwise_equipotent
by A5, CLASSES1:84;
A47:
FinS F,Y = ((FinS F,Y) | n) ^ <*(F . d)*>
by A7, A10, RFINSEQ:20;
then A48:
FinS F,(Y \ {d}),(FinS F,Y) | n are_fiberwise_equipotent
by A46, RFINSEQ:14;
(FinS F,Y) | n is non-increasing
by RFINSEQ:33;
hence
FinS F,X = (FinS F,Y) ^ (FinS F,(X \ Y))
by A45, A47, A48, RFINSEQ:36; :: thesis: verum