let D be non empty set ; :: thesis: for F being PartFunc of D,REAL
for X being set
for r being Real
for Z being finite set st Z = dom (F | X) & rng (F | X) = {r} holds
FinS F,X = (card Z) |-> r
let F be PartFunc of D,REAL ; :: thesis: for X being set
for r being Real
for Z being finite set st Z = dom (F | X) & rng (F | X) = {r} holds
FinS F,X = (card Z) |-> r
let X be set ; :: thesis: for r being Real
for Z being finite set st Z = dom (F | X) & rng (F | X) = {r} holds
FinS F,X = (card Z) |-> r
let r be Real; :: thesis: for Z being finite set st Z = dom (F | X) & rng (F | X) = {r} holds
FinS F,X = (card Z) |-> r
let dx be finite set ; :: thesis: ( dx = dom (F | X) & rng (F | X) = {r} implies FinS F,X = (card dx) |-> r )
assume A1: dx = dom (F | X) ; :: thesis: ( not rng (F | X) = {r} or FinS F,X = (card dx) |-> r )
set fx = FinS F,X;
assume A2: rng (F | X) = {r} ; :: thesis: FinS F,X = (card dx) |-> r
F | X, FinS F,X are_fiberwise_equipotent by A1, Def14;
then A3: rng (FinS F,X) = {r} by A2, CLASSES1:83;
( len (FinS F,X) = card dx & dom (FinS F,X) = Seg (len (FinS F,X)) ) by A1, Th70, FINSEQ_1:def 3;
hence FinS F,X = (card dx) |-> r by A3, FUNCOP_1:15; :: thesis: verum