let C, D 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 (Rland (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 (Rland (F,A)) = C
let A be RearrangmentGen of C; :: thesis: ( F is total & card C = card D implies dom (Rland (F,A)) = C )
A1: ( len (CHI (A,C)) = len A & len A <> 0 ) by Th4, RFUNCT_3:def 6;
assume ( F is total & card C = card D ) ; :: thesis: dom (Rland (F,A)) = C
then A2: len (MIM (FinS (F,D))) = len (CHI (A,C)) by Th11;
thus dom (Rland (F,A)) c= C ; :: according to XBOOLE_0:def 10 :: thesis: C c= dom (Rland (F,A))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in C or x in dom (Rland (F,A)) )
assume x in C ; :: thesis: x in dom (Rland (F,A))
then reconsider c = x as Element of C ;
( len ((MIM (FinS (F,D))) (#) (CHI (A,C))) = min ((len (MIM (FinS (F,D)))),(len (CHI (A,C)))) & c is_common_for_dom (MIM (FinS (F,D))) (#) (CHI (A,C)) ) by RFUNCT_3:32, RFUNCT_3:def 7;
hence x in dom (Rland (F,A)) by A2, A1, RFUNCT_3:28; :: thesis: verum