let D be non empty set ; :: thesis: for F being PartFunc of D,REAL
for d being Element of D st d in dom F holds
FinS F,{d} = <*(F . d)*>
let F be PartFunc of D,REAL ; :: thesis: for d being Element of D st d in dom F holds
FinS F,{d} = <*(F . d)*>
let d be Element of D; :: thesis: ( d in dom F implies FinS F,{d} = <*(F . d)*> )
assume d in dom F ; :: thesis: FinS F,{d} = <*(F . d)*>
then {d} c= dom F by ZFMISC_1:37;
then A1: {d} = (dom F) /\ {d} by XBOOLE_1:28
.= dom (F | {d}) by RELAT_1:90 ;
then FinS F,{d},F | {d} are_fiberwise_equipotent by Def14;
then A2: rng (FinS F,{d}) = rng (F | {d}) by CLASSES1:83;
A3: rng (F | {d}) = {(F . d)}

proof

thus rng (F | {d}) c= {(F . d)} :: according to XBOOLE_0:def 10 :: thesis: {(F . d)} c= rng (F | {d})

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (F | {d}) or x in {(F . d)} )
assume x in rng (F | {d}) ; :: thesis: x in {(F . d)}
then consider e being Element of D such that
A4: e in dom (F | {d}) and
A5: (F | {d}) . e = x by PARTFUN1:26;
e = d by A1, A4, TARSKI:def 1;
then x = F . d by A4, A5, FUNCT_1:70;
hence x in {(F . d)} by TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(F . d)} or x in rng (F | {d}) )
A6: d in dom (F | {d}) by A1, TARSKI:def 1;
assume x in {(F . d)} ; :: thesis: x in rng (F | {d})
then x = F . d by TARSKI:def 1;
then x = (F | {d}) . d by A6, FUNCT_1:70;
hence x in rng (F | {d}) by A6, FUNCT_1:def 5; :: thesis: verum

end;

len (FinS F,{d}) = card {d} by A1, Th70
.= 1 by CARD_1:50 ;
hence FinS F,{d} = <*(F . d)*> by A2, A3, FINSEQ_1:56; :: thesis: verum