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, Def13;
then A3: rng (FinS (F,X)) = {r} by A2, CLASSES1:75;
A4: dom (FinS (F,X)) = Seg (len (FinS (F,X))) by FINSEQ_1:def 3;
len (FinS (F,X)) = card dx by A1, Th67;
hence FinS (F,X) = (card dx) |-> r by A3, A4, FUNCOP_1:9; :: thesis: verum