let D be non empty set ; :: thesis: for F being PartFunc of D,REAL
for X being set
for d being Element of D st dom (F | X) is finite & d in dom (F | X) & (FinS F,X) . (len (FinS F,X)) = F . d holds
FinS F,X = (FinS F,(X \ {d})) ^ <*(F . d)*>
let F be PartFunc of D,REAL ; :: thesis: for X being set
for d being Element of D st dom (F | X) is finite & d in dom (F | X) & (FinS F,X) . (len (FinS F,X)) = F . d holds
FinS F,X = (FinS F,(X \ {d})) ^ <*(F . d)*>
let X be set ; :: thesis: for d being Element of D st dom (F | X) is finite & d in dom (F | X) & (FinS F,X) . (len (FinS F,X)) = F . d holds
FinS F,X = (FinS F,(X \ {d})) ^ <*(F . d)*>
let d be Element of D; :: thesis: ( dom (F | X) is finite & d in dom (F | X) & (FinS F,X) . (len (FinS F,X)) = F . d implies FinS F,X = (FinS F,(X \ {d})) ^ <*(F . d)*> )
set dx = dom (F | X);
set fx = FinS F,X;
set fy = FinS F,(X \ {d});
assume A1: ( dom (F | X) is finite & d in dom (F | X) & (FinS F,X) . (len (FinS F,X)) = F . d ) ; :: thesis: FinS F,X = (FinS F,(X \ {d})) ^ <*(F . d)*>
then A2: FinS F,X,F | X are_fiberwise_equipotent by Def14;
then A3: rng (FinS F,X) = rng (F | X) by CLASSES1:83;
(FinS F,(X \ {d})) ^ <*(F . d)*>,F | X are_fiberwise_equipotent by A1, Th69;
then A4: FinS F,X,(FinS F,(X \ {d})) ^ <*(F . d)*> are_fiberwise_equipotent by A2, CLASSES1:84;
FinS F,X <> {} by A1, A3, FUNCT_1:12, RELAT_1:60;
then ( len (FinS F,X) <> 0 & 0 <= len (FinS F,X) ) ;
then 0 + 1 <= len (FinS F,X) by NAT_1:13;
then max 0 ,((len (FinS F,X)) - 1) = (len (FinS F,X)) - 1 by FINSEQ_2:4;
then reconsider n = (len (FinS F,X)) - 1 as Element of NAT by FINSEQ_2:5;
len (FinS F,X) = n + 1 ;
then A5: FinS F,X = ((FinS F,X) | n) ^ <*(F . d)*> by A1, RFINSEQ:20;
then A6: FinS F,(X \ {d}),(FinS F,X) | n are_fiberwise_equipotent by A4, RFINSEQ:14;
(FinS F,X) | n is non-increasing by RFINSEQ:33;
hence FinS F,X = (FinS F,(X \ {d})) ^ <*(F . d)*> by A5, A6, RFINSEQ:36; :: thesis: verum