let C, D be non empty finite set ; 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; 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; ( 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 )
; FinS ((Rlor (F,B)),C) = FinS (F,D)
then A2:
Rlor (F,B), FinS (F,D) are_fiberwise_equipotent
by Th23;
A3:
dom (Rlor (F,B)) = C
by A1, Th20;
then
(Rlor (F,B)) | C = Rlor (F,B)
by RELAT_1:68;
hence
FinS ((Rlor (F,B)),C) = FinS (F,D)
by A2, A3, RFUNCT_3:def 13; verum