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
( 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 2;
dom (F | D) = (dom F) /\ D by RELAT_1:61
.= D by A3 ;
then A4: FinS (F,D),F | D are_fiberwise_equipotent by RFUNCT_3:def 13;
Rlor (F,A), FinS (F,D) are_fiberwise_equipotent by A1, A2, Th23;
then A5: Rlor (F,A),F | D are_fiberwise_equipotent by A4, CLASSES1:76;
Rland (F,A), FinS (F,D) are_fiberwise_equipotent by A1, A2, Th16;
then Rland (F,A),F | D are_fiberwise_equipotent by A4, CLASSES1:76;
hence ( Rland (F,A),F are_fiberwise_equipotent & Rlor (F,A),F are_fiberwise_equipotent ) by A3, A5, RELAT_1:68; :: 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:75; :: thesis: verum