let D be non empty set ; 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; 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 ; for Y being finite set st Y = dom (F | X) holds
len (FinS (F,X)) = card Y
let Y be finite set ; ( 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)
; 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
;
verum