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 that
A2: dy = dom (F | Y) and
A3: dom (F | X) is finite and
A4: Y c= X and
A5: n + 1 = card dy and
A6: 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))
A7: len (FinS F,Y) = n + 1 by A2, A5, Th70;
A8: F | Y, FinS F,Y are_fiberwise_equipotent by A2, Def14;
then A9: rng (FinS F,Y) = rng (F | Y) by CLASSES1:83;
0 + 1 <= n + 1 by NAT_1:13;
then A10: len (FinS F,Y) in dom (FinS F,Y) by A7, 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
A11: d in dy and
A12: (F | Y) . d = (FinS F,Y) . (len (FinS F,Y)) by A2, A9, PARTFUN1:26;
A13: dom (F | (X \ Y)) = (dom F) /\ (X \ Y) by RELAT_1:90;
A14: dy = (dom F) /\ Y by A2, RELAT_1:90;
then A15: d in Y by A11, XBOOLE_0:def 4;
then A16: {d} c= X by A4, ZFMISC_1:37;
A17: d in dom F by A14, A11, XBOOLE_0:def 4;
then A18: {d} c= dom F by ZFMISC_1:37;
A19: {d} c= Y by A15, ZFMISC_1:37;
A20: (FinS F,(X \ Y)) ^ <*(F . d)*>,<*(F . d)*> ^ (FinS F,(X \ Y)) are_fiberwise_equipotent by RFINSEQ:15;
set Yd = Y \ {d};
set dyd = dom (F | (Y \ {d}));
set xyd = dom (F | (X \ (Y \ {d})));
A21: dom (F | (X \ (Y \ {d}))) = (dom F) /\ (X \ (Y \ {d})) by RELAT_1:90;
A22: dom (F | (Y \ {d})) = (dom F) /\ (Y \ {d}) by RELAT_1:90;
A23: dom (F | (Y \ {d})) = dy \ {d}
proof
thus dom (F | (Y \ {d})) c= dy \ {d} :: according to XBOOLE_0:def 10 :: thesis: dy \ {d} c= dom (F | (Y \ {d}))
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in dom (F | (Y \ {d})) or y in dy \ {d} )
assume A24: y in dom (F | (Y \ {d})) ; :: thesis: y in dy \ {d}
then y in Y \ {d} by A22, XBOOLE_0:def 4;
then A25: not y in {d} by XBOOLE_0:def 5;
y in dom F by A22, A24, XBOOLE_0:def 4;
then y in dy by A14, A22, A24, XBOOLE_0:def 4;
hence y in dy \ {d} by A25, XBOOLE_0:def 5; :: thesis: verum
end;
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in dy \ {d} or y in dom (F | (Y \ {d})) )
assume A26: y in dy \ {d} ; :: thesis: y in dom (F | (Y \ {d}))
then ( not y in {d} & y in Y ) by A14, XBOOLE_0:def 4, XBOOLE_0:def 5;
then A27: y in Y \ {d} by XBOOLE_0:def 5;
y in dom F by A14, A26, XBOOLE_0:def 4;
hence y in dom (F | (Y \ {d})) by A22, A27, XBOOLE_0:def 4; :: thesis: verum
end;
A28: F . d = (FinS F,Y) . (len (FinS F,Y)) by A2, A11, A12, FUNCT_1:70;
then A29: FinS F,Y = ((FinS F,Y) | n) ^ <*(F . d)*> by A7, RFINSEQ:20;
reconsider dyd = dom (F | (Y \ {d})) as finite set by A23;
A30: X \ (Y \ {d}) = (X \ Y) \/ (X /\ {d}) by XBOOLE_1:52
.= (X \ Y) \/ {d} by A16, XBOOLE_1:28 ;
then A31: dom (F | (X \ (Y \ {d}))) = (dom (F | (X \ Y))) \/ ((dom F) /\ {d}) by A13, A21, XBOOLE_1:23
.= (dom (F | (X \ Y))) \/ {d} by A18, XBOOLE_1:28 ;
A32: 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 that
A33: d1 in dyd and
A34: d2 in dom (F | (X \ (Y \ {d}))) ; :: thesis: F . d1 >= F . d2
now
per cases ( d2 in dom (F | (X \ Y)) or d2 in {d} ) by A31, A34, XBOOLE_0:def 3;
case d2 in dom (F | (X \ Y)) ; :: thesis: F . d1 >= F . d2
hence F . d1 >= F . d2 by A2, A6, A23, A33; :: thesis: verum
end;
case d2 in {d} ; :: thesis: F . d1 >= F . d2
then A35: d2 = d by TARSKI:def 1;
(F | Y) . d1 in rng (F | Y) by A2, A23, A33, FUNCT_1:def 5;
then F . d1 in rng (F | Y) by A2, A23, A33, FUNCT_1:70;
then consider m being Nat such that
A36: m in dom (FinS F,Y) and
A37: (FinS F,Y) . m = F . d1 by A9, FINSEQ_2:11;
A38: m <= len (FinS F,Y) by A36, FINSEQ_3:27;
now
per cases ( m = len (FinS F,Y) or m <> len (FinS F,Y) ) ;
case m = len (FinS F,Y) ; :: thesis: F . d1 >= F . d2
hence F . d1 >= F . d2 by A2, A11, A12, A35, A37, FUNCT_1:70; :: thesis: verum
end;
case m <> len (FinS F,Y) ; :: thesis: F . d1 >= F . d2
then m < len (FinS F,Y) by A38, XXREAL_0:1;
hence F . d1 >= F . d2 by A10, A28, A35, A36, A37, RFINSEQ:32; :: thesis: verum
end;
end;
end;
hence F . d1 >= F . d2 ; :: thesis: verum
end;
end;
end;
hence F . d1 >= F . d2 ; :: thesis: verum
end;
dom (F | X) = (dom F) /\ X by RELAT_1:90;
then A39: dom (F | (X \ Y)) is finite by A3, A13, FINSET_1:13, XBOOLE_1:26;
then F | (X \ Y), FinS F,(X \ Y) are_fiberwise_equipotent by Def14;
then A40: rng (FinS F,(X \ Y)) = rng (F | (X \ Y)) by CLASSES1:83;
A41: <*(F . d)*> ^ (FinS F,(X \ Y)) is non-increasing
proof
set xfy = <*(F . d)*> ^ (FinS F,(X \ Y));
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 that
A42: n in dom (<*(F . d)*> ^ (FinS F,(X \ Y))) and
A43: 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
A44: 1 <= n by A42, 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;
set r = (<*(F . d)*> ^ (FinS F,(X \ Y))) . n;
set s = (<*(F . d)*> ^ (FinS F,(X \ Y))) . (n + 1);
A45: len <*(F . d)*> = 1 by FINSEQ_1:57;
then len (<*(F . d)*> ^ (FinS F,(X \ Y))) = 1 + (len (FinS F,(X \ Y))) by FINSEQ_1:35;
then A46: len (FinS F,(X \ Y)) = (len (<*(F . d)*> ^ (FinS F,(X \ Y)))) - 1 ;
A47: n + 1 <= len (<*(F . d)*> ^ (FinS F,(X \ Y))) by A43, FINSEQ_3:27;
then n1 + 1 <= len (FinS F,(X \ Y)) by A46, XREAL_1:21;
then A48: n1 + 1 in dom (FinS F,(X \ Y)) by A44, FINSEQ_3:27;
then (FinS F,(X \ Y)) . (n1 + 1) in rng (FinS F,(X \ Y)) by FUNCT_1:def 5;
then consider d1 being Element of D such that
A49: ( d1 in dom (F | (X \ Y)) & (F | (X \ Y)) . d1 = (FinS F,(X \ Y)) . (n1 + 1) ) by A40, PARTFUN1:26;
1 < n + 1 by A44, NAT_1:13;
then A50: (<*(F . d)*> ^ (FinS F,(X \ Y))) . (n + 1) = (FinS F,(X \ Y)) . ((n + 1) - 1) by A45, A47, FINSEQ_1:37
.= (FinS F,(X \ Y)) . (n1 + 1) ;
A51: n <= len (<*(F . d)*> ^ (FinS F,(X \ Y))) by A42, FINSEQ_3:27;
then A52: n1 <= len (FinS F,(X \ Y)) by A46, XREAL_1:11;
A53: ( F . d1 = (FinS F,(X \ Y)) . (n1 + 1) & F . d >= F . d1 ) by A2, A6, A11, A49, FUNCT_1:70;
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)
hence (<*(F . d)*> ^ (FinS F,(X \ Y))) . n >= (<*(F . d)*> ^ (FinS F,(X \ Y))) . (n + 1) by A50, A53, FINSEQ_1:58; :: thesis: verum
end;
suppose n <> 1 ; :: thesis: (<*(F . d)*> ^ (FinS F,(X \ Y))) . n >= (<*(F . d)*> ^ (FinS F,(X \ Y))) . (n + 1)
then A54: 1 < n by A44, XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then 1 <= n1 by XREAL_1:21;
then A55: n1 in dom (FinS F,(X \ Y)) by A52, FINSEQ_3:27;
(<*(F . d)*> ^ (FinS F,(X \ Y))) . n = (FinS F,(X \ Y)) . n1 by A45, A51, A54, FINSEQ_1:37;
hence (<*(F . d)*> ^ (FinS F,(X \ Y))) . n >= (<*(F . d)*> ^ (FinS F,(X \ Y))) . (n + 1) by A48, A50, A55, RFINSEQ:def 4; :: thesis: verum
end;
end;
end;
hence (<*(F . d)*> ^ (FinS F,(X \ Y))) . n >= (<*(F . d)*> ^ (FinS F,(X \ Y))) . (n + 1) ; :: thesis: verum
end;
d in {d} by TARSKI:def 1;
then d in X \ (Y \ {d}) by A30, XBOOLE_0:def 3;
then A56: d in dom (F | (X \ (Y \ {d}))) by A21, A17, XBOOLE_0:def 4;
(X \ (Y \ {d})) \ {d} = X \ ((Y \ {d}) \/ {d}) by XBOOLE_1:41
.= X \ (Y \/ {d}) by XBOOLE_1:39
.= X \ Y by A19, XBOOLE_1:12 ;
then (FinS F,(X \ Y)) ^ <*(F . d)*>,F | (X \ (Y \ {d})) are_fiberwise_equipotent by A39, A31, A56, Th69;
then <*(F . d)*> ^ (FinS F,(X \ Y)),F | (X \ (Y \ {d})) are_fiberwise_equipotent by A20, CLASSES1:84;
then A57: <*(F . d)*> ^ (FinS F,(X \ Y)) = FinS F,(X \ (Y \ {d})) by A39, A31, A41, Def14;
{d} c= dy by A11, ZFMISC_1:37;
then card dyd = (card dy) - (card {d}) by A23, CARD_2:63
.= (n + 1) - 1 by A5, CARD_1:50
.= n ;
then FinS F,X = (FinS F,(Y \ {d})) ^ (FinS F,(X \ (Y \ {d}))) by A1, A3, A4, A32, XBOOLE_1:1;
then A58: FinS F,X = ((FinS F,(Y \ {d})) ^ <*(F . d)*>) ^ (FinS F,(X \ Y)) by A57, FINSEQ_1:45;
A59: (FinS F,Y) | n is non-increasing by RFINSEQ:33;
F | Y,(FinS F,(Y \ {d})) ^ <*(F . d)*> are_fiberwise_equipotent by A2, A11, Th69;
then (FinS F,(Y \ {d})) ^ <*(F . d)*>, FinS F,Y are_fiberwise_equipotent by A8, CLASSES1:84;
then FinS F,(Y \ {d}),(FinS F,Y) | n are_fiberwise_equipotent by A29, RFINSEQ:14;
hence FinS F,X = (FinS F,Y) ^ (FinS F,(X \ Y)) by A58, A29, A59, RFINSEQ:36; :: thesis: verum