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
dom (Rlor F,A) = C
let F be PartFunc of D,REAL ; :: thesis: 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; :: thesis: ( F is total & card C = card D implies dom (Rlor F,B) = C )
set b = Co_Gen B;
assume A1: ( F is total & card C = card D ) ; :: thesis: dom (Rlor F,B) = C
thus dom (Rlor F,B) c= C ; :: according to XBOOLE_0:def 10 :: thesis: C c= dom (Rlor F,B)
A2: ( len (MIM (FinS F,D)) = len (CHI (Co_Gen B),C) & len (CHI (Co_Gen B),C) = len (Co_Gen B) & len B <> 0 & len ((MIM (FinS F,D)) (#) (CHI (Co_Gen B),C)) = min (len (MIM (FinS F,D))),(len (CHI (Co_Gen B),C)) & len (Co_Gen B) = card D & len B = card D ) by A1, Th1, Th12, RFUNCT_3:def 6, RFUNCT_3:def 7;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in C or x in dom (Rlor F,B) )
assume x in C ; :: thesis: 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:35;
hence x in dom (Rlor F,B) by A2, RFUNCT_3:31; :: thesis: verum