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 D = card C holds
( len (FinS ((Rlor (F,A)),C)) = card C & 1 <= len (FinS ((Rlor (F,A)),C)) )
let F be PartFunc of D,REAL; :: thesis: for A being RearrangmentGen of C st F is total & card D = card C holds
( len (FinS ((Rlor (F,A)),C)) = card C & 1 <= len (FinS ((Rlor (F,A)),C)) )
let B be RearrangmentGen of C; :: thesis: ( F is total & card D = card C implies ( len (FinS ((Rlor (F,B)),C)) = card C & 1 <= len (FinS ((Rlor (F,B)),C)) ) )
set p = Rlor (F,B);
assume ( F is total & card D = card C ) ; :: thesis: ( len (FinS ((Rlor (F,B)),C)) = card C & 1 <= len (FinS ((Rlor (F,B)),C)) )
then A1: dom (Rlor (F,B)) = C by Th20;
then A2: (Rlor (F,B)) | C = Rlor (F,B) by RELAT_1:68;
hence len (FinS ((Rlor (F,B)),C)) = card C by A1, RFUNCT_3:67; :: thesis: 1 <= len (FinS ((Rlor (F,B)),C))
0 + 1 <= card C by NAT_1:13;
hence 1 <= len (FinS ((Rlor (F,B)),C)) by A1, A2, RFUNCT_3:67; :: thesis: verum