let D be non empty set ; :: thesis: for F being PartFunc of D,REAL
for r being Real
for X being set
for Z being finite set st Z = dom (F | X) holds
FinS (F - r),X = (FinS F,X) - ((card Z) |-> r)
let F be PartFunc of D,REAL ; :: thesis: for r being Real
for X being set
for Z being finite set st Z = dom (F | X) holds
FinS (F - r),X = (FinS F,X) - ((card Z) |-> r)
let r be Real; :: thesis: for X being set
for Z being finite set st Z = dom (F | X) holds
FinS (F - r),X = (FinS F,X) - ((card Z) |-> r)
let X be set ; :: thesis: for Z being finite set st Z = dom (F | X) holds
FinS (F - r),X = (FinS F,X) - ((card Z) |-> r)
let G be finite set ; :: thesis: ( G = dom (F | X) implies FinS (F - r),X = (FinS F,X) - ((card G) |-> r) )
assume A1: G = dom (F | X) ; :: thesis: FinS (F - r),X = (FinS F,X) - ((card G) |-> r)
defpred S2[ Element of NAT ] means for X being set
for G being finite set st G = dom (F | X) & $1 = card G holds
FinS (F - r),X = (FinS F,X) - ((card G) |-> r);
A2: S2[ 0 ]
proof
let X be set ; :: thesis: for G being finite set st G = dom (F | X) & 0 = card G holds
FinS (F - r),X = (FinS F,X) - ((card G) |-> r)
let G be finite set ; :: thesis: ( G = dom (F | X) & 0 = card G implies FinS (F - r),X = (FinS F,X) - ((card G) |-> r) )
assume A3: G = dom (F | X) ; :: thesis: ( not 0 = card G or FinS (F - r),X = (FinS F,X) - ((card G) |-> r) )
assume 0 = card G ; :: thesis: FinS (F - r),X = (FinS F,X) - ((card G) |-> r)
then A4: dom (F | X) = {} by A3;
then FinS F,X = FinS F,{} by Th66
.= <*> REAL by Th71 ;
then A5: (FinS F,X) - ((card G) |-> r) = <*> REAL by FINSEQ_2:87;
dom ((F - r) | X) = (dom (F - r)) /\ X by RELAT_1:90
.= (dom F) /\ X by VALUED_1:3
.= dom (F | X) by RELAT_1:90 ;
hence FinS (F - r),X = FinS (F - r),{} by A4, Th66
.= (FinS F,X) - ((card G) |-> r) by A5, Th71 ;
:: thesis: verum
end;
A6: for n being Element of NAT st S2[n] holds
S2[n + 1]
proof
let n be Element of NAT ; :: thesis: ( S2[n] implies S2[n + 1] )
assume A7: S2[n] ; :: thesis: S2[n + 1]
let X be set ; :: thesis: for G being finite set st G = dom (F | X) & n + 1 = card G holds
FinS (F - r),X = (FinS F,X) - ((card G) |-> r)
let G be finite set ; :: thesis: ( G = dom (F | X) & n + 1 = card G implies FinS (F - r),X = (FinS F,X) - ((card G) |-> r) )
assume A8: G = dom (F | X) ; :: thesis: ( not n + 1 = card G or FinS (F - r),X = (FinS F,X) - ((card G) |-> r) )
assume A9: n + 1 = card G ; :: thesis: FinS (F - r),X = (FinS F,X) - ((card G) |-> r)
A10: dom ((F - r) | X) = (dom (F - r)) /\ X by RELAT_1:90
.= (dom F) /\ X by VALUED_1:3
.= dom (F | X) by RELAT_1:90 ;
then A11: FinS (F - r),X,(F - r) | X are_fiberwise_equipotent by A8, Def14;
then A12: rng (FinS (F - r),X) = rng ((F - r) | X) by CLASSES1:83;
A13: 0 + 1 <= n + 1 by NAT_1:13;
set frx = FinS (F - r),X;
set fx = FinS F,X;
A14: ( len (FinS (F - r),X) = card G & len (FinS F,X) = card G ) by A8, A10, Th70;
then len (FinS (F - r),X) in dom (FinS (F - r),X) by A9, A13, FINSEQ_3:27;
then (FinS (F - r),X) . (len (FinS (F - r),X)) in rng (FinS (F - r),X) by FUNCT_1:def 5;
then consider d being Element of D such that
A15: ( d in dom ((F - r) | X) & ((F - r) | X) . d = (FinS (F - r),X) . (len (FinS (F - r),X)) ) by A12, PARTFUN1:26;
(F - r) . d = (FinS (F - r),X) . (len (FinS (F - r),X)) by A15, FUNCT_1:70;
then A16: (FinS F,X) . (len (FinS F,X)) = F . d by A8, A10, A15, Th75;
set Y = X \ {d};
set dx = dom (F | X);
set dy = dom (F | (X \ {d}));
set fry = FinS (F - r),(X \ {d});
set fy = FinS F,(X \ {d});
set n1r = (n + 1) |-> r;
set nr = n |-> r;
( FinS F,X = (FinS F,(X \ {d})) ^ <*(F . d)*> & FinS F,X = ((FinS F,X) | n) ^ <*(F . d)*> ) by A8, A9, A10, A14, A15, A16, Th73, RFINSEQ:20;
then A17: FinS F,(X \ {d}) = (FinS F,X) | n by FINSEQ_1:46;
(F - r) . d = (FinS (F - r),X) . (len (FinS (F - r),X)) by A15, FUNCT_1:70;
then A18: FinS (F - r),X = ((FinS (F - r),X) | n) ^ <*((F - r) . d)*> by A9, A14, RFINSEQ:20;
A19: (FinS (F - r),X) | n is non-increasing by RFINSEQ:33;
(FinS (F - r),(X \ {d})) ^ <*((F - r) . d)*>,(F - r) | X are_fiberwise_equipotent by A8, A10, A15, Th69;
then (FinS (F - r),(X \ {d})) ^ <*((F - r) . d)*>, FinS (F - r),X are_fiberwise_equipotent by A11, CLASSES1:84;
then FinS (F - r),(X \ {d}),(FinS (F - r),X) | n are_fiberwise_equipotent by A18, RFINSEQ:14;
then A20: FinS (F - r),(X \ {d}) = (FinS (F - r),X) | n by A19, RFINSEQ:36;
A21: ( {d} c= dom (F | X) & dom (F | (X \ {d})) = (dom F) /\ (X \ {d}) & dom (F | X) = (dom F) /\ X & dom ((F - r) | X) = (dom (F - r)) /\ X ) by A10, A15, RELAT_1:90, ZFMISC_1:37;
A22: dom (F | (X \ {d})) = (dom (F | X)) \ {d}
proof
thus dom (F | (X \ {d})) c= (dom (F | X)) \ {d} :: according to XBOOLE_0:def 10 :: thesis: (dom (F | X)) \ {d} c= dom (F | (X \ {d}))
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in dom (F | (X \ {d})) or y in (dom (F | X)) \ {d} )
assume y in dom (F | (X \ {d})) ; :: thesis: y in (dom (F | X)) \ {d}
then A23: ( y in dom F & y in X \ {d} ) by A21, XBOOLE_0:def 4;
then A24: ( y in X & not y in {d} ) by XBOOLE_0:def 5;
y in dom (F | X) by A21, A23, XBOOLE_0:def 4;
hence y in (dom (F | X)) \ {d} by A24, XBOOLE_0:def 5; :: thesis: verum
end;
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in (dom (F | X)) \ {d} or y in dom (F | (X \ {d})) )
assume y in (dom (F | X)) \ {d} ; :: thesis: y in dom (F | (X \ {d}))
then A25: ( y in dom (F | X) & not y in {d} ) by XBOOLE_0:def 5;
then A26: ( y in dom F & y in X ) by A21, XBOOLE_0:def 4;
then y in X \ {d} by A25, XBOOLE_0:def 5;
hence y in dom (F | (X \ {d})) by A21, A26, XBOOLE_0:def 4; :: thesis: verum
end;
then reconsider dx = dom (F | X), dy = dom (F | (X \ {d})) as finite set by A8;
A27: card dy = (card dx) - (card {d}) by A21, A22, CARD_2:63
.= (n + 1) - 1 by A8, A9, CARD_1:50
.= n ;
then A28: FinS (F - r),(X \ {d}) = (FinS F,(X \ {d})) - (n |-> r) by A7;
d in dom (F - r) by A15, A21, XBOOLE_0:def 4;
then d in dom F by VALUED_1:3;
then (F - r) . d = (F . d) - r by VALUED_1:3;
then A29: <*((F - r) . d)*> = <*(F . d)*> - <*r*> by RVSUM_1:50;
A30: ( len ((n + 1) |-> r) = n + 1 & len (n |-> r) = n ) by FINSEQ_1:def 18;
A31: ( len (FinS F,X) = n + 1 & len (FinS F,(X \ {d})) = n ) by A8, A9, A27, Th70;
then A32: len ((FinS F,X) - ((n + 1) |-> r)) = n + 1 by A30, FINSEQ_2:86;
A33: len ((FinS F,(X \ {d})) - (n |-> r)) = n by A30, A31, FINSEQ_2:86;
A34: ( len <*(F . d)*> = 1 & len <*r*> = 1 & <*(F . d)*> . 1 = F . d & <*r*> . 1 = r & <*(F . d)*> - <*r*> = diffreal .: <*(F . d)*>,<*r*> ) by FINSEQ_1:57;
then A35: len (<*(F . d)*> - <*r*>) = 1 by FINSEQ_2:86;
then A36: len (((FinS F,(X \ {d})) - (n |-> r)) ^ (<*(F . d)*> - <*r*>)) = n + 1 by A33, FINSEQ_1:35;
A37: dom (FinS F,X) = Seg (len (FinS F,X)) by FINSEQ_1:def 3;
A38: ( dom (<*(F . d)*> - <*r*>) = dom (<*(F . d)*> - <*r*>) & dom ((FinS F,(X \ {d})) - (n |-> r)) = Seg (len ((FinS F,(X \ {d})) - (n |-> r))) & n + 1 in Seg (n + 1) ) by FINSEQ_1:6, FINSEQ_1:def 3;
A39: ( n < n + 1 & 1 in Seg 1 ) by FINSEQ_1:3, NAT_1:13;
then A40: 1 in dom (<*(F . d)*> - <*r*>) by A35, FINSEQ_1:def 3;
X: dom ((FinS F,X) - ((n + 1) |-> r)) = Seg (n + 1) by A32, FINSEQ_1:def 3;
now
let m be Nat; :: thesis: ( m in dom ((FinS F,X) - ((n + 1) |-> r)) implies ((FinS F,X) - ((n + 1) |-> r)) . b1 = (((FinS F,(X \ {d})) - (n |-> r)) ^ (<*(F . d)*> - <*r*>)) . b1 )
assume A41: m in dom ((FinS F,X) - ((n + 1) |-> r)) ; :: thesis: ((FinS F,X) - ((n + 1) |-> r)) . b1 = (((FinS F,(X \ {d})) - (n |-> r)) ^ (<*(F . d)*> - <*r*>)) . b1
per cases ( m = n + 1 or m <> n + 1 ) ;
suppose A42: m = n + 1 ; :: thesis: ((FinS F,X) - ((n + 1) |-> r)) . b1 = (((FinS F,(X \ {d})) - (n |-> r)) ^ (<*(F . d)*> - <*r*>)) . b1
then A43: ((n + 1) |-> r) . m = r by FINSEQ_1:6, FUNCOP_1:13;
(((FinS F,(X \ {d})) - (n |-> r)) ^ (<*(F . d)*> - <*r*>)) . m = (<*(F . d)*> - <*r*>) . ((n + 1) - n) by A33, A36, A39, A42, FINSEQ_1:37
.= (F . d) - r by A34, A40, VALUED_1:13 ;
hence ((FinS F,X) - ((n + 1) |-> r)) . m = (((FinS F,(X \ {d})) - (n |-> r)) ^ (<*(F . d)*> - <*r*>)) . m by A16, A31, A42, A43, A41, VALUED_1:13; :: thesis: verum
end;
suppose A45: m <> n + 1 ; :: thesis: (((FinS F,(X \ {d})) - (n |-> r)) ^ (<*(F . d)*> - <*r*>)) . b1 = ((FinS F,X) - ((n + 1) |-> r)) . b1
A46: ( 1 <= m & m <= n + 1 ) by A41, X, FINSEQ_1:3;
then m < n + 1 by A45, XXREAL_0:1;
then A47: m <= n by NAT_1:13;
then A48: m in Seg n by A46, FINSEQ_1:3;
then A49: (((FinS F,(X \ {d})) - (n |-> r)) ^ (<*(F . d)*> - <*r*>)) . m = ((FinS F,(X \ {d})) - (n |-> r)) . m by A33, A38, FINSEQ_1:def 7;
A50: (n |-> r) . m = r by A48, FUNCOP_1:13;
( 1 <= n & n <= n + 1 ) by A46, A47, NAT_1:11, XXREAL_0:2;
then n in Seg (n + 1) by FINSEQ_1:3;
then A51: ( ((FinS F,X) | n) . m = (FinS F,X) . m & m in dom (FinS F,X) & ((n + 1) |-> r) . m = r ) by A31, A37, A41, A48, X, FUNCOP_1:13, RFINSEQ:19;
reconsider s = (FinS F,X) . m as Real ;
m in dom ((FinS F,(X \ {d})) - (n |-> r)) by A33, A48, FINSEQ_1:def 3;
hence (((FinS F,(X \ {d})) - (n |-> r)) ^ (<*(F . d)*> - <*r*>)) . m = s - r by A17, A49, A50, A51, VALUED_1:13
.= ((FinS F,X) - ((n + 1) |-> r)) . m by A51, A41, VALUED_1:13 ;
:: thesis: verum
end;
end;
end;
hence FinS (F - r),X = (FinS F,X) - ((card G) |-> r) by A9, A18, A20, A28, A29, A32, A36, FINSEQ_2:10; :: thesis: verum
end;
for n being Element of NAT holds S2[n] from NAT_1:sch 1(A2, A6);
 hence FinS (F - r),X = (FinS F,X) - ((card G) |-> r) by A1; :: thesis: verum