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
FinS (Rlor 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 (Rlor F,A),C = FinS F,D
let B be RearrangmentGen of C; :: thesis: ( F is total & card C = card D implies FinS (Rlor F,B),C = FinS F,D )
assume A1: ( F is total & card C = card D ) ; :: thesis: FinS (Rlor F,B),C = FinS F,D
then A2: Rlor F,B, FinS F,D are_fiberwise_equipotent by Th24;
A3: dom (Rlor F,B) = C by A1, Th21;
then (Rlor F,B) | C = Rlor F,B by RELAT_1:97;
hence FinS (Rlor F,B),C = FinS F,D by A2, A3, RFUNCT_3:def 14; :: thesis: verum