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:90
.= (dom F) /\ X by VALUED_1:3
.= dx by RELAT_1:90 ;
then FinS F,X,F | X are_fiberwise_equipotent by Def14;
then A4: rng (FinS F,X) = rng (F | X) by CLASSES1:83;
then FinS F,X <> {} by A2, FUNCT_1:12, RELAT_1:60;
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:27;
(F | X) . d in rng (F | X) by A2, FUNCT_1:def 5;
then F . d in rng (F | X) by A2, FUNCT_1:70;
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:11;
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, Def14;
then A9: rng (FinS (F - r),X) = rng ((F - r) | X) by CLASSES1:83;
A10: ( len (FinS F,X) = card dx & dom (FinS (F - r),X) = Seg (len (FinS (F - r),X)) ) by Th70, FINSEQ_1:def 3;
A11: len (FinS (F - r),X) = card dx by A3, Th70;
then (FinS (F - r),X) . (len (FinS (F - r),X)) in rng (FinS (F - r),X) by A10, A8, A5, FUNCT_1:def 5;
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:26;
(F | X) . d1 = F . d1 by A3, A12, FUNCT_1:70;
then F . d1 in rng (F | X) by A3, A12, FUNCT_1:def 5;
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:11;
A16: dom (F - r) = dom F by VALUED_1:3;
A17: dom ((F - r) | X) = (dom (F - r)) /\ X by RELAT_1:90;
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:70
.= (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:27;
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 5;
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:26;
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:70;
((F - r) | X) . d1 = (F - r) . d1 by A3, A23, FUNCT_1:70
.= (F . d1) - r by A16, A25, VALUED_1:3 ;
then (F . d1) - r in rng ((F - r) | X) by A3, A23, FUNCT_1:def 5;
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:11;
A29: m <= len (FinS (F - r),X) by A27, FINSEQ_3:27;
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:32;

now

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:70; :: 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:32;
then F . d1 >= F . d by XREAL_1:11;
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 5;
then (F - r) . d in rng ((F - r) | X) by A2, A3, FUNCT_1:70;
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:11;
n1 <= len (FinS (F - r),X) by A35, FINSEQ_3:27;
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:32;
then A37: F . d >= F . d1 by XREAL_1:11;
A38: m <= len (FinS F,X) by A14, FINSEQ_3:27;

now

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:32;
hence contradiction by A21, A34, A19, A37, XXREAL_0:1; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum