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 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 Th21;
then A2: (Rlor F,B) | C = Rlor F,B by RELAT_1:97;
hence len (FinS (Rlor F,B),C) = card C by A1, RFUNCT_3:70; :: 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:70; :: thesis: verum