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 4;
then reconsider F9 = F as finite Function by FINSET_1:29;
reconsider da9 = dom a9, dF9 = dom F9 as finite set ;
A4: F | D = F by A3, RELAT_1:97;
D = (dom F) /\ D by A3
.= dom (F | D) by RELAT_1:90 ;
then F, FinS F,D are_fiberwise_equipotent by A4, RFUNCT_3:def 14;
then A5: ( dom (FinS F,D) = Seg (len (FinS F,D)) & card da9 = card dF9 ) by CLASSES1:89, 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:78
.= len (MIM (FinS F,D)) by RFINSEQ:def 3 ; :: thesis: verum