let C, D be non empty finite set ; for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card C = card D holds
len (MIM (FinS (F,D))) = len (CHI (A,C))
let F be PartFunc of D,REAL; for A being RearrangmentGen of C st F is total & card C = card D holds
len (MIM (FinS (F,D))) = len (CHI (A,C))
let A be RearrangmentGen of C; ( F is total & card C = card D implies len (MIM (FinS (F,D))) = len (CHI (A,C)) )
assume that
A1:
F is total
and
A2:
card C = card D
; len (MIM (FinS (F,D))) = len (CHI (A,C))
set a = FinS (F,D);
reconsider a9 = FinS (F,D) as finite Function ;
A3:
dom F = D
by A1, PARTFUN1:def 2;
then reconsider F9 = F as finite Function by FINSET_1:10;
reconsider da9 = dom a9, dF9 = dom F9 as finite set ;
A4:
F | D = F
by A3, RELAT_1:68;
D =
(dom F) /\ D
by A3
.=
dom (F | D)
by RELAT_1:61
;
then
F, FinS (F,D) are_fiberwise_equipotent
by A4, RFUNCT_3:def 13;
then A5:
( dom (FinS (F,D)) = Seg (len (FinS (F,D))) & card da9 = card dF9 )
by CLASSES1:81, FINSEQ_1:def 3;
thus len (CHI (A,C)) =
len A
by RFUNCT_3:def 6
.=
card C
by Th1
.=
len (FinS (F,D))
by A2, A3, A5, FINSEQ_1:57
.=
len (MIM (FinS (F,D)))
by RFINSEQ:def 2
; verum