let C, D 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
FinS ((Rland (F,A)),C) = FinS (F,D)
let F be PartFunc of D,REAL; :: thesis: for A being RearrangmentGen of C st F is total & card C = card D holds
FinS ((Rland (F,A)),C) = FinS (F,D)
let B be RearrangmentGen of C; :: thesis: ( F is total & card C = card D implies FinS ((Rland (F,B)),C) = FinS (F,D) )
assume A1: ( F is total & card C = card D ) ; :: thesis: FinS ((Rland (F,B)),C) = FinS (F,D)
then A2: Rland (F,B), FinS (F,D) are_fiberwise_equipotent by Th16;
A3: dom (Rland (F,B)) = C by A1, Th12;
then (Rland (F,B)) | C = Rland (F,B) by RELAT_1:68;
hence FinS ((Rland (F,B)),C) = FinS (F,D) by A2, A3, RFUNCT_3:def 13; :: thesis: verum