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
( Rland F,A,F are_fiberwise_equipotent & Rlor F,A,F are_fiberwise_equipotent & rng (Rland F,A) = rng F & rng (Rlor F,A) = rng F )
let F be PartFunc of D,REAL ; :: thesis: for A being RearrangmentGen of C st F is total & card D = card C holds
( Rland F,A,F are_fiberwise_equipotent & Rlor F,A,F are_fiberwise_equipotent & rng (Rland F,A) = rng F & rng (Rlor F,A) = rng F )
let A be RearrangmentGen of C; :: thesis: ( F is total & card D = card C implies ( Rland F,A,F are_fiberwise_equipotent & Rlor F,A,F are_fiberwise_equipotent & rng (Rland F,A) = rng F & rng (Rlor F,A) = rng F ) )
assume A1: ( F is total & card D = card C ) ; :: thesis: ( Rland F,A,F are_fiberwise_equipotent & Rlor F,A,F are_fiberwise_equipotent & rng (Rland F,A) = rng F & rng (Rlor F,A) = rng F )
then A2: ( Rland F,A, FinS F,D are_fiberwise_equipotent & Rlor F,A, FinS F,D are_fiberwise_equipotent ) by Th17, Th24;
A3: dom F = D by A1, PARTFUN1:def 4;
dom (F | D) = (dom F) /\ D by RELAT_1:90
.= D by A3 ;
then FinS F,D,F | D are_fiberwise_equipotent by RFUNCT_3:def 14;
then ( Rland F,A,F | D are_fiberwise_equipotent & Rlor F,A,F | D are_fiberwise_equipotent ) by A2, CLASSES1:84;
hence ( Rland F,A,F are_fiberwise_equipotent & Rlor F,A,F are_fiberwise_equipotent ) by A3, RELAT_1:97; :: thesis: ( rng (Rland F,A) = rng F & rng (Rlor F,A) = rng F )
hence ( rng (Rland F,A) = rng F & rng (Rlor F,A) = rng F ) by CLASSES1:83; :: thesis: verum