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, Def14;
then rng (FinS F,X) = rng (F | X) by CLASSES1:83;
then FinS F,X <> {} by A2, FUNCT_1:12, RELAT_1:60;
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:20;
A6: (FinS F,X) | n is non-increasing by RFINSEQ:33;
(FinS F,(X \ {d})) ^ <*(F . d)*>,F | X are_fiberwise_equipotent by A1, A2, Th69;
then FinS F,X,(FinS F,(X \ {d})) ^ <*(F . d)*> are_fiberwise_equipotent by A4, CLASSES1:84;
then FinS F,(X \ {d}),(FinS F,X) | n are_fiberwise_equipotent by A5, RFINSEQ:14;
hence FinS F,X = (FinS F,(X \ {d})) ^ <*(F . d)*> by A5, A6, RFINSEQ:36; :: thesis: verum