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 A1: ( dom (F | X) is finite & 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 )
then reconsider dx = dom (F | X) as finite set ;
A2: dom (F - r) = dom F by VALUED_1:3;
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 A4: ( len (FinS (F - r),X) = card dx & len (FinS F,X) = card dx ) by Th70;
A5: ( dom (FinS (F - r),X) = Seg (len (FinS (F - r),X)) & dom (FinS F,X) = Seg (len (FinS F,X)) ) by FINSEQ_1:def 3;
( FinS F,X,F | X are_fiberwise_equipotent & FinS (F - r),X,(F - r) | X are_fiberwise_equipotent ) by A3, Def14;
then A6: ( rng (FinS F,X) = rng (F | X) & rng (FinS (F - r),X) = rng ((F - r) | X) ) by CLASSES1:83;
A7: ( dom ((F - r) | X) = (dom (F - r)) /\ X & dx = (dom F) /\ X ) by RELAT_1:90;
then A8: d in dom (F - r) by A1, A3, XBOOLE_0:def 4;
then A9: (F - r) . d = (F . d) - r by A2, VALUED_1:3;
A10: (F | X) . d in rng (F | X) by A1, FUNCT_1:def 5;
FinS F,X <> {} by A1, A6, FUNCT_1:12, RELAT_1:60;
then ( len (FinS F,X) <> 0 & 0 <= len (FinS F,X) ) ;
then 0 + 1 <= len (FinS F,X) by NAT_1:13;
then A11: len (FinS F,X) in dom (FinS F,X) by FINSEQ_3:27;
F . d in rng (F | X) by A1, A10, FUNCT_1:70;
then consider n being Nat such that
A12: ( n in dom (FinS F,X) & (FinS F,X) . n = F . d ) by A6, FINSEQ_2:11;
A13: ( 1 <= n & n <= len (FinS F,X) ) by A12, 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
assume that
A14: (FinS (F - r),X) . (len (FinS (F - r),X)) = (F - r) . d and
A15: (FinS F,X) . (len (FinS F,X)) <> F . d ; :: thesis: contradiction
(FinS F,X) . (len (FinS F,X)) in rng (FinS F,X) by A11, FUNCT_1:def 5;
then consider d1 being Element of D such that
A16: ( d1 in dx & (F | X) . d1 = (FinS F,X) . (len (FinS F,X)) ) by A6, PARTFUN1:26;
A17: F . d1 = (FinS F,X) . (len (FinS F,X)) by A16, FUNCT_1:70;
A18: d1 in dom (F - r) by A3, A7, A16, XBOOLE_0:def 4;
((F - r) | X) . d1 = (F - r) . d1 by A3, A16, FUNCT_1:70
.= (F . d1) - r by A2, A18, VALUED_1:3 ;
then (F . d1) - r in rng ((F - r) | X) by A3, A16, FUNCT_1:def 5;
then consider m being Nat such that
A19: ( m in dom (FinS (F - r),X) & (FinS (F - r),X) . m = (F . d1) - r ) by A6, FINSEQ_2:11;
A20: ( 1 <= m & m <= len (FinS (F - r),X) ) by A19, FINSEQ_3:27;
n < len (FinS F,X) by A12, A13, A15, XXREAL_0:1;
then A21: F . d >= F . d1 by A11, A12, A17, 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 A2, A8, A14, A19, VALUED_1:3;
hence contradiction by A15, A16, FUNCT_1:70; :: thesis: verum
end;
case len (FinS (F - r),X) <> m ; :: thesis: contradiction
then m < len (FinS (F - r),X) by A20, XXREAL_0:1;
then (F . d1) - r >= (F . d) - r by A4, A5, A9, A11, A14, A19, RFINSEQ:32;
then F . d1 >= F . d by XREAL_1:11;
hence contradiction by A15, A17, A21, XXREAL_0:1; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
assume that
A22: (FinS F,X) . (len (FinS F,X)) = F . d and
A23: (FinS (F - r),X) . (len (FinS (F - r),X)) <> (F - r) . d ; :: thesis: contradiction
(FinS (F - r),X) . (len (FinS (F - r),X)) in rng (FinS (F - r),X) by A4, A5, A11, FUNCT_1:def 5;
then consider d1 being Element of D such that
A24: ( d1 in dom ((F - r) | X) & ((F - r) | X) . d1 = (FinS (F - r),X) . (len (FinS (F - r),X)) ) by A6, PARTFUN1:26;
A25: d1 in dom (F - r) by A7, A24, XBOOLE_0:def 4;
A26: (FinS (F - r),X) . (len (FinS (F - r),X)) = (F - r) . d1 by A24, FUNCT_1:70
.= (F . d1) - r by A2, A25, VALUED_1:3 ;
(F | X) . d1 = F . d1 by A3, A24, FUNCT_1:70;
then F . d1 in rng (F | X) by A3, A24, FUNCT_1:def 5;
then consider m being Nat such that
A27: ( m in dom (FinS F,X) & (FinS F,X) . m = F . d1 ) by A6, FINSEQ_2:11;
A28: ( 1 <= m & m <= len (FinS F,X) ) by A27, FINSEQ_3:27;
((F - r) | X) . d in rng ((F - r) | X) by A1, A3, FUNCT_1:def 5;
then (F - r) . d in rng ((F - r) | X) by A1, A3, FUNCT_1:70;
then consider n1 being Nat such that
A29: ( n1 in dom (FinS (F - r),X) & (FinS (F - r),X) . n1 = (F . d) - r ) by A6, A9, FINSEQ_2:11;
( 1 <= n1 & n1 <= len (FinS (F - r),X) ) by A29, FINSEQ_3:27;
then n1 < len (FinS (F - r),X) by A9, A23, A29, XXREAL_0:1;
then (F . d) - r >= (F . d1) - r by A4, A5, A11, A26, A29, RFINSEQ:32;
then A30: F . d >= F . d1 by XREAL_1:11;
now
per cases ( len (FinS F,X) = m or len (FinS F,X) <> m ) ;
end;
end;
hence contradiction ; :: thesis: verum