let n be 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, Th67;
A8: F | Y, FinS (F,Y) are_fiberwise_equipotent by A2, Def13;
then A9: rng (FinS (F,Y)) = rng (F | Y) by CLASSES1:75;
0 + 1 <= n + 1 by NAT_1:13;
then A10: len (FinS (F,Y)) in dom (FinS (F,Y)) by A7, FINSEQ_3:25;
then (FinS (F,Y)) . (len (FinS (F,Y))) in rng (FinS (F,Y)) by FUNCT_1:def 3;
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:3;
A13: dom (F | (X \ Y)) = (dom F) /\ (X \ Y) by RELAT_1:61;
A14: dy = (dom F) /\ Y by A2, RELAT_1:61;
then A15: d in Y by A11, XBOOLE_0:def 4;
then A16: {d} c= X by A4, ZFMISC_1:31;
A17: d in dom F by A14, A11, XBOOLE_0:def 4;
then A18: {d} c= dom F by ZFMISC_1:31;
A19: {d} c= Y by A15, ZFMISC_1:31;
A20: (FinS (F,(X \ Y))) ^ <*(F . d)*>,<*(F . d)*> ^ (FinS (F,(X \ Y))) are_fiberwise_equipotent by RFINSEQ:2;
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:61;
A22: dom (F | (Y \ {d})) = (dom F) /\ (Y \ {d}) by RELAT_1:61;
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 object ; :: 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 object ; :: 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:47;
then A29: FinS (F,Y) = ((FinS (F,Y)) | n) ^ <*(F . d)*> by A7, RFINSEQ:7;
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 :: thesis: for d1, d2 being Element of D st d1 in dyd & d2 in dom (F | (X \ (Y \ {d}))) holds
F . d1 >= F . d2
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 :: thesis: ( ( d2 in dom (F | (X \ Y)) & F . d1 >= F . d2 ) or ( d2 in {d} & F . d1 >= F . d2 ) )
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 3;
then F . d1 in rng (F | Y) by A2, A23, A33, FUNCT_1:47;
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:10;
A38: m <= len (FinS (F,Y)) by A36, FINSEQ_3:25;
now :: thesis: ( ( m = len (FinS (F,Y)) & F . d1 >= F . d2 ) or ( m <> len (FinS (F,Y)) & F . d1 >= F . d2 ) )
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:47; :: 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:19; :: 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:61;
then A39: dom (F | (X \ Y)) is finite by A3, A13, FINSET_1:1, XBOOLE_1:26;
then F | (X \ Y), FinS (F,(X \ Y)) are_fiberwise_equipotent by Def13;
then A40: rng (FinS (F,(X \ Y))) = rng (F | (X \ Y)) by CLASSES1:75;
A41: <*(F . d)*> ^ (FinS (F,(X \ Y))) is non-increasing
proof
set xfy = <*(F . d)*> ^ (FinS (F,(X \ Y)));
let n be Nat; :: according to RFINSEQ:def 3 :: 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:25;
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:40;
then len (<*(F . d)*> ^ (FinS (F,(X \ Y)))) = 1 + (len (FinS (F,(X \ Y)))) by FINSEQ_1:22;
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:25;
then n1 + 1 <= len (FinS (F,(X \ Y))) by A46, XREAL_1:19;
then A48: n1 + 1 in dom (FinS (F,(X \ Y))) by A44, FINSEQ_3:25;
then (FinS (F,(X \ Y))) . (n1 + 1) in rng (FinS (F,(X \ Y))) by FUNCT_1:def 3;
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:3;
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:24
.= (FinS (F,(X \ Y))) . (n1 + 1) ;
A51: n <= len (<*(F . d)*> ^ (FinS (F,(X \ Y)))) by A42, FINSEQ_3:25;
then A52: n1 <= len (FinS (F,(X \ Y))) by A46, XREAL_1:9;
A53: ( F . d1 = (FinS (F,(X \ Y))) . (n1 + 1) & F . d >= F . d1 ) by A2, A6, A11, A49, FUNCT_1:47;
now :: thesis: (<*(F . d)*> ^ (FinS (F,(X \ Y)))) . n >= (<*(F . d)*> ^ (FinS (F,(X \ Y)))) . (n + 1)
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:41; :: 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:19;
then A55: n1 in dom (FinS (F,(X \ Y))) by A52, FINSEQ_3:25;
(<*(F . d)*> ^ (FinS (F,(X \ Y)))) . n = (FinS (F,(X \ Y))) . n1 by A45, A51, A54, FINSEQ_1:24;
hence (<*(F . d)*> ^ (FinS (F,(X \ Y)))) . n >= (<*(F . d)*> ^ (FinS (F,(X \ Y)))) . (n + 1) by A48, A50, A55, RFINSEQ:def 3; :: thesis: verum
end;
end;
end;
hence (<*(F . d)*> ^ (FinS (F,(X \ Y)))) . n >= (<*(F . d)*> ^ (FinS (F,(X \ Y)))) . (n + 1) ; :: thesis: verum
end;
A56: <*(F . d)*> ^ (FinS (F,(X \ Y))) is FinSequence of REAL by RVSUM_1:145;
d in {d} by TARSKI:def 1;
then d in X \ (Y \ {d}) by A30, XBOOLE_0:def 3;
then A57: 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, A57, Th66;
then <*(F . d)*> ^ (FinS (F,(X \ Y))),F | (X \ (Y \ {d})) are_fiberwise_equipotent by A20, CLASSES1:76;
then A58: <*(F . d)*> ^ (FinS (F,(X \ Y))) = FinS (F,(X \ (Y \ {d}))) by A39, A31, A41, Def13, A56;
{d} c= dy by A11, ZFMISC_1:31;
then card dyd = (card dy) - (card {d}) by A23, CARD_2:44
.= (n + 1) - 1 by A5, CARD_1:30
.= n ;
then FinS (F,X) = (FinS (F,(Y \ {d}))) ^ (FinS (F,(X \ (Y \ {d})))) by A1, A3, A4, A32, XBOOLE_1:1;
then A59: FinS (F,X) = ((FinS (F,(Y \ {d}))) ^ <*(F . d)*>) ^ (FinS (F,(X \ Y))) by A58, FINSEQ_1:32;
A60: (FinS (F,Y)) | n is non-increasing by RFINSEQ:20;
F | Y,(FinS (F,(Y \ {d}))) ^ <*(F . d)*> are_fiberwise_equipotent by A2, A11, Th66;
then (FinS (F,(Y \ {d}))) ^ <*(F . d)*>, FinS (F,Y) are_fiberwise_equipotent by A8, CLASSES1:76;
then FinS (F,(Y \ {d})),(FinS (F,Y)) | n are_fiberwise_equipotent by A29, RFINSEQ:1;
hence FinS (F,X) = (FinS (F,Y)) ^ (FinS (F,(X \ Y))) by A59, A29, A60, RFINSEQ:23; :: thesis: verum