let D be non empty set ; :: thesis: for F being PartFunc of D,REAL
for X being set
for Y being finite set st Y = dom (F | X) holds
len (FinS F,X) = card Y
let F be PartFunc of D,REAL ; :: thesis: for X being set
for Y being finite set st Y = dom (F | X) holds
len (FinS F,X) = card Y
let X be set ; :: thesis: for Y being finite set st Y = dom (F | X) holds
len (FinS F,X) = card Y
let Y be finite set ; :: thesis: ( Y = dom (F | X) implies len (FinS F,X) = card Y )
reconsider fs = dom (FinS F,X) as finite set ;
A1: dom (FinS F,X) = Seg (len (FinS F,X)) by FINSEQ_1:def 3;
assume A2: Y = dom (F | X) ; :: thesis: len (FinS F,X) = card Y
then reconsider fx = F | X as finite Function by FINSET_1:29;
FinS F,X,F | X are_fiberwise_equipotent by A2, Def14;
hence card Y = card fs by A2, CLASSES1:89
.= len (FinS F,X) by A1, FINSEQ_1:78 ;
:: thesis: verum