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 )
assume A1: Y = dom (F | X) ; :: thesis: len (FinS F,X) = card Y
then reconsider fx = F | X as finite Function by FINSET_1:29;
A2: Y = dom fx by A1;
A3: FinS F,X,F | X are_fiberwise_equipotent by A1, Def14;
reconsider fs = dom (FinS F,X) as finite set ;
A4: dom (FinS F,X) = Seg (len (FinS F,X)) by FINSEQ_1:def 3;
thus card Y = card fs by A2, A3, CLASSES1:89
.= len (FinS F,X) by A4, FINSEQ_1:78 ; :: thesis: verum