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:31;
then A1: {d} = (dom F) /\ {d} by XBOOLE_1:28
.= dom (F | {d}) by RELAT_1:61 ;
then FinS (F,{d}),F | {d} are_fiberwise_equipotent by Def13;
then A2: rng (FinS (F,{d})) = rng (F | {d}) by CLASSES1:75;
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 object ; :: 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:3;
e = d by A1, A4, TARSKI:def 1;
then x = F . d by A4, A5, FUNCT_1:47;
hence x in {(F . d)} by TARSKI:def 1; :: thesis: verum
end;
let x be object ; :: 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:47;
hence x in rng (F | {d}) by A6, FUNCT_1:def 3; :: thesis: verum
end;
len (FinS (F,{d})) = card {d} by A1, Th67
.= 1 by CARD_1:30 ;
hence FinS (F,{d}) = <*(F . d)*> by A2, A3, FINSEQ_1:39; :: thesis: verum