let D, C be non empty finite set ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: verum