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 that
A1: dom (F | X) is finite and
A2: d in dom (F | X) and
A3: (FinS (F,X)) . (len (FinS (F,X))) = F . d ; :: thesis: FinS (F,X) = (FinS (F,(X \ {d}))) ^ <*(F . d)*>
A4: FinS (F,X),F | X are_fiberwise_equipotent by A1, Def13;
then rng (FinS (F,X)) = rng (F | X) by CLASSES1:75;
then FinS (F,X) <> {} by A2, FUNCT_1:3, RELAT_1:38;
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 A3, RFINSEQ:7;
A6: (FinS (F,X)) | n is non-increasing by RFINSEQ:20;
(FinS (F,(X \ {d}))) ^ <*(F . d)*>,F | X are_fiberwise_equipotent by A1, A2, Th66;
then FinS (F,X),(FinS (F,(X \ {d}))) ^ <*(F . d)*> are_fiberwise_equipotent by A4, CLASSES1:76;
then FinS (F,(X \ {d})),(FinS (F,X)) | n are_fiberwise_equipotent by A5, RFINSEQ:1;
hence FinS (F,X) = (FinS (F,(X \ {d}))) ^ <*(F . d)*> by A5, A6, RFINSEQ:23; :: thesis: verum