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 (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 Th17;
A3: dom (Rland F,B) = C by A1, Th13;
then (Rland F,B) | C = Rland F,B by RELAT_1:97;
hence FinS (Rland F,B),C = FinS F,D by A2, A3, RFUNCT_3:def 14; :: thesis: verum