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
FinS (F,X),F | X are_fiberwise_equipotent by A2, Def13;
hence card Y = card fs by A2, CLASSES1:81
.= len (FinS (F,X)) by A1, FINSEQ_1:57 ;
:: thesis: verum