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