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
dom (Rlor (F,A)) = C
let F be PartFunc of D,REAL; for A being RearrangmentGen of C st F is total & card C = card D holds
dom (Rlor (F,A)) = C
let B be RearrangmentGen of C; ( F is total & card C = card D implies dom (Rlor (F,B)) = C )
set b = Co_Gen B;
A1:
( len (CHI ((Co_Gen B),C)) = len (Co_Gen B) & len ((MIM (FinS (F,D))) (#) (CHI ((Co_Gen B),C))) = min ((len (MIM (FinS (F,D)))),(len (CHI ((Co_Gen B),C)))) )
by RFUNCT_3:def 6, RFUNCT_3:def 7;
assume
( F is total & card C = card D )
; dom (Rlor (F,B)) = C
then A2:
( len (MIM (FinS (F,D))) = len (CHI ((Co_Gen B),C)) & len (Co_Gen B) = card D )
by Th1, Th11;
thus
dom (Rlor (F,B)) c= C
; XBOOLE_0:def 10 C c= dom (Rlor (F,B))
let x be object ; TARSKI:def 3 ( not x in C or x in dom (Rlor (F,B)) )
assume
x in C
; x in dom (Rlor (F,B))
then reconsider c = x as Element of C ;
c is_common_for_dom (MIM (FinS (F,D))) (#) (CHI ((Co_Gen B),C))
by RFUNCT_3:32;
hence
x in dom (Rlor (F,B))
by A1, A2, RFUNCT_3:28; verum