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 A1: ( F is total & card C = card D ) ; :: thesis: len (MIM (FinS F,D)) = len (CHI A,C)
then A2: dom F = D by PARTFUN1:def 4;
then reconsider F' = F as finite Function by FINSET_1:29;
A3: D = (dom F) /\ D by A2
.= dom (F | D) by RELAT_1:90 ;
F | D = F by A2, RELAT_1:97;
then A4: F, FinS F,D are_fiberwise_equipotent by A3, RFUNCT_3:def 14;
set a = FinS F,D;
A5: dom (FinS F,D) = Seg (len (FinS F,D)) by FINSEQ_1:def 3;
reconsider a' = FinS F,D as finite Function ;
reconsider da' = dom a', dF' = dom F' as finite set ;
A6: card da' = card dF' by A4, CLASSES1:89;
thus len (CHI A,C) = len A by RFUNCT_3:def 6
.= card C by Th1
.= len (FinS F,D) by A1, A2, A5, A6, FINSEQ_1:78
.= len (MIM (FinS F,D)) by RFINSEQ:def 3 ; :: thesis: verum