let D be non empty set ; :: thesis: for F being PartFunc of D,REAL
for r being Real
for X being set
for d being Element of D st dom (F | X) is finite & d in dom (F | X) holds
( (FinS ((F - r),X)) . (len (FinS ((F - r),X))) = (F - r) . d iff (FinS (F,X)) . (len (FinS (F,X))) = F . d )
let F be PartFunc of D,REAL; :: thesis: for r being Real
for X being set
for d being Element of D st dom (F | X) is finite & d in dom (F | X) holds
( (FinS ((F - r),X)) . (len (FinS ((F - r),X))) = (F - r) . d iff (FinS (F,X)) . (len (FinS (F,X))) = F . d )
let r be Real; :: thesis: for X being set
for d being Element of D st dom (F | X) is finite & d in dom (F | X) holds
( (FinS ((F - r),X)) . (len (FinS ((F - r),X))) = (F - r) . d iff (FinS (F,X)) . (len (FinS (F,X))) = F . d )
let X be set ; :: thesis: for d being Element of D st dom (F | X) is finite & d in dom (F | X) holds
( (FinS ((F - r),X)) . (len (FinS ((F - r),X))) = (F - r) . d iff (FinS (F,X)) . (len (FinS (F,X))) = F . d )
let d be Element of D; :: thesis: ( dom (F | X) is finite & d in dom (F | X) implies ( (FinS ((F - r),X)) . (len (FinS ((F - r),X))) = (F - r) . d iff (FinS (F,X)) . (len (FinS (F,X))) = F . d ) )
set dx = dom (F | X);
set drx = dom ((F - r) | X);
set frx = FinS ((F - r),X);
set fx = FinS (F,X);
assume that
A1: dom (F | X) is finite and
A2: d in dom (F | X) ; :: thesis: ( (FinS ((F - r),X)) . (len (FinS ((F - r),X))) = (F - r) . d iff (FinS (F,X)) . (len (FinS (F,X))) = F . d )
reconsider dx = dom (F | X) as finite set by A1;
A3: dom ((F - r) | X) = (dom (F - r)) /\ X by RELAT_1:61
.= (dom F) /\ X by VALUED_1:3
.= dx by RELAT_1:61 ;
then FinS (F,X),F | X are_fiberwise_equipotent by Def13;
then A4: rng (FinS (F,X)) = rng (F | X) by CLASSES1:75;
then FinS (F,X) <> {} by A2, FUNCT_1:3, RELAT_1:38;
then 0 + 1 <= len (FinS (F,X)) by NAT_1:13;
then A5: len (FinS (F,X)) in dom (FinS (F,X)) by FINSEQ_3:25;
(F | X) . d in rng (F | X) by A2, FUNCT_1:def 3;
then F . d in rng (F | X) by A2, FUNCT_1:47;
then consider n being Nat such that
A6: n in dom (FinS (F,X)) and
A7: (FinS (F,X)) . n = F . d by A4, FINSEQ_2:10;
A8: dom (FinS (F,X)) = Seg (len (FinS (F,X))) by FINSEQ_1:def 3;
FinS ((F - r),X),(F - r) | X are_fiberwise_equipotent by A3, Def13;
then A9: rng (FinS ((F - r),X)) = rng ((F - r) | X) by CLASSES1:75;
A10: ( len (FinS (F,X)) = card dx & dom (FinS ((F - r),X)) = Seg (len (FinS ((F - r),X))) ) by Th67, FINSEQ_1:def 3;
A11: len (FinS ((F - r),X)) = card dx by A3, Th67;
then (FinS ((F - r),X)) . (len (FinS ((F - r),X))) in rng (FinS ((F - r),X)) by A10, A8, A5, FUNCT_1:def 3;
then consider d1 being Element of D such that
A12: d1 in dom ((F - r) | X) and
A13: ((F - r) | X) . d1 = (FinS ((F - r),X)) . (len (FinS ((F - r),X))) by A9, PARTFUN1:3;
(F | X) . d1 = F . d1 by A3, A12, FUNCT_1:47;
then F . d1 in rng (F | X) by A3, A12, FUNCT_1:def 3;
then consider m being Nat such that
A14: m in dom (FinS (F,X)) and
A15: (FinS (F,X)) . m = F . d1 by A4, FINSEQ_2:10;
A16: dom (F - r) = dom F by VALUED_1:3;
A17: dom ((F - r) | X) = (dom (F - r)) /\ X by RELAT_1:61;
then A18: d1 in dom (F - r) by A12, XBOOLE_0:def 4;
A19: (FinS ((F - r),X)) . (len (FinS ((F - r),X))) = (F - r) . d1 by A12, A13, FUNCT_1:47
.= (F . d1) - r by A16, A18, VALUED_1:3 ;
A20: d in dom (F - r) by A2, A3, A17, XBOOLE_0:def 4;
then A21: (F - r) . d = (F . d) - r by A16, VALUED_1:3;
A22: n <= len (FinS (F,X)) by A6, FINSEQ_3:25;
thus ( (FinS ((F - r),X)) . (len (FinS ((F - r),X))) = (F - r) . d implies (FinS (F,X)) . (len (FinS (F,X))) = F . d ) :: thesis: ( (FinS (F,X)) . (len (FinS (F,X))) = F . d implies (FinS ((F - r),X)) . (len (FinS ((F - r),X))) = (F - r) . d )

proof

(FinS (F,X)) . (len (FinS (F,X))) in rng (FinS (F,X)) by A5, FUNCT_1:def 3;
then consider d1 being Element of D such that
A23: d1 in dx and
A24: (F | X) . d1 = (FinS (F,X)) . (len (FinS (F,X))) by A4, PARTFUN1:3;
A25: d1 in dom (F - r) by A3, A17, A23, XBOOLE_0:def 4;
A26: F . d1 = (FinS (F,X)) . (len (FinS (F,X))) by A23, A24, FUNCT_1:47;
((F - r) | X) . d1 = (F - r) . d1 by A3, A23, FUNCT_1:47
.= (F . d1) - r by A16, A25, VALUED_1:3 ;
then (F . d1) - r in rng ((F - r) | X) by A3, A23, FUNCT_1:def 3;
then consider m being Nat such that
A27: m in dom (FinS ((F - r),X)) and
A28: (FinS ((F - r),X)) . m = (F . d1) - r by A9, FINSEQ_2:10;
A29: m <= len (FinS ((F - r),X)) by A27, FINSEQ_3:25;
assume that
A30: (FinS ((F - r),X)) . (len (FinS ((F - r),X))) = (F - r) . d and
A31: (FinS (F,X)) . (len (FinS (F,X))) <> F . d ; :: thesis: contradiction
n < len (FinS (F,X)) by A7, A22, A31, XXREAL_0:1;
then A32: F . d >= F . d1 by A5, A6, A7, A26, RFINSEQ:19;

now :: thesis: ( ( len (FinS ((F - r),X)) = m & contradiction ) or ( len (FinS ((F - r),X)) <> m & contradiction ) )

per cases ( len (FinS ((F - r),X)) = m or len (FinS ((F - r),X)) <> m ) ;

case len (FinS ((F - r),X)) = m ; :: thesis: contradiction

then (F . d1) + (- r) = (F . d) - r by A16, A20, A30, A28, VALUED_1:3;
hence contradiction by A31, A23, A24, FUNCT_1:47; :: thesis: verum

end;

case len (FinS ((F - r),X)) <> m ; :: thesis: contradiction

then m < len (FinS ((F - r),X)) by A29, XXREAL_0:1;
then (F . d1) - r >= (F . d) - r by A11, A10, A8, A21, A5, A30, A27, A28, RFINSEQ:19;
then F . d1 >= F . d by XREAL_1:9;
hence contradiction by A31, A26, A32, XXREAL_0:1; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

assume that
A33: (FinS (F,X)) . (len (FinS (F,X))) = F . d and
A34: (FinS ((F - r),X)) . (len (FinS ((F - r),X))) <> (F - r) . d ; :: thesis: contradiction
((F - r) | X) . d in rng ((F - r) | X) by A2, A3, FUNCT_1:def 3;
then (F - r) . d in rng ((F - r) | X) by A2, A3, FUNCT_1:47;
then consider n1 being Nat such that
A35: n1 in dom (FinS ((F - r),X)) and
A36: (FinS ((F - r),X)) . n1 = (F . d) - r by A9, A21, FINSEQ_2:10;
n1 <= len (FinS ((F - r),X)) by A35, FINSEQ_3:25;
then n1 < len (FinS ((F - r),X)) by A21, A34, A36, XXREAL_0:1;
then (F . d) - r >= (F . d1) - r by A11, A10, A8, A5, A19, A35, A36, RFINSEQ:19;
then A37: F . d >= F . d1 by XREAL_1:9;
A38: m <= len (FinS (F,X)) by A14, FINSEQ_3:25;

now :: thesis: ( ( len (FinS (F,X)) = m & contradiction ) or ( len (FinS (F,X)) <> m & contradiction ) )

per cases ( len (FinS (F,X)) = m or len (FinS (F,X)) <> m ) ;

case len (FinS (F,X)) = m ; :: thesis: contradiction

hence contradiction by A16, A20, A33, A34, A19, A15, VALUED_1:3; :: thesis: verum

end;

case len (FinS (F,X)) <> m ; :: thesis: contradiction

then m < len (FinS (F,X)) by A38, XXREAL_0:1;
then F . d1 >= F . d by A5, A33, A14, A15, RFINSEQ:19;
hence contradiction by A21, A34, A19, A37, XXREAL_0:1; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum