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 that
A1: F is total and
A2: 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 )
A3: dom F = D by A1, PARTFUN1:def 4;
dom (F | D) = (dom F) /\ D by RELAT_1:90
.= D by A3 ;
then A4: FinS F,D,F | D are_fiberwise_equipotent by RFUNCT_3:def 14;
Rlor F,A, FinS F,D are_fiberwise_equipotent by A1, A2, Th24;
then A5: Rlor F,A,F | D are_fiberwise_equipotent by A4, CLASSES1:84;
Rland F,A, FinS F,D are_fiberwise_equipotent by A1, A2, Th17;
then Rland F,A,F | D are_fiberwise_equipotent by A4, CLASSES1:84;
hence ( Rland F,A,F are_fiberwise_equipotent & Rlor F,A,F are_fiberwise_equipotent ) by A3, A5, 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