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)
reconsider rr = r as Element of REAL by XREAL_0:def 1;
defpred S2[ 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);
A1: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume A2: 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 A3: G = dom (F | X) ; :: thesis: ( not n + 1 = card G or FinS ((F - r),X) = (FinS (F,X)) - ((card G) |-> r) )
set frx = FinS ((F - rr),X);
set fx = FinS (F,X);
A4: dom ((F - r) | X) = (dom (F - r)) /\ X by RELAT_1:61
.= (dom F) /\ X by VALUED_1:3
.= dom (F | X) by RELAT_1:61 ;
then A5: len (FinS ((F - rr),X)) = card G by A3, Th67;
A6: FinS ((F - r),X),(F - r) | X are_fiberwise_equipotent by A3, A4, Def13;
then A7: rng (FinS ((F - r),X)) = rng ((F - r) | X) by CLASSES1:75;
assume A8: n + 1 = card G ; :: thesis: FinS ((F - r),X) = (FinS (F,X)) - ((card G) |-> r)
then A9: len (FinS (F,X)) = n + 1 by A3, Th67;
0 + 1 <= n + 1 by NAT_1:13;
then len (FinS ((F - rr),X)) in dom (FinS ((F - rr),X)) by A8, A5, FINSEQ_3:25;
then (FinS ((F - rr),X)) . (len (FinS ((F - rr),X))) in rng (FinS ((F - rr),X)) by FUNCT_1:def 3;
then consider d being Element of D such that
A10: d in dom ((F - r) | X) and
A11: ((F - r) | X) . d = (FinS ((F - rr),X)) . (len (FinS ((F - rr),X))) by A7, PARTFUN1:3;
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) |-> rr;
set nr = n |-> rr;
A12: {d} c= dom (F | X) by A4, A10, ZFMISC_1:31;
(F - r) . d = (FinS ((F - rr),X)) . (len (FinS ((F - rr),X))) by A10, A11, FUNCT_1:47;
then A13: (FinS (F,X)) . (len (FinS (F,X))) = F . d by A3, A4, A10, Th72;
len (FinS (F,X)) = card G by A3, Th67;
then A14: FinS (F,X) = ((FinS (F,X)) | n) ^ <*(F . d)*> by A8, A13, RFINSEQ:7;
FinS (F,X) = (FinS (F,(X \ {d}))) ^ <*(F . d)*> by A3, A4, A10, A13, Th70;
then A15: FinS (F,(X \ {d})) = (FinS (F,X)) | n by A14, FINSEQ_1:33;
A16: dom ((FinS (F,(X \ {d}))) - (n |-> rr)) = Seg (len ((FinS (F,(X \ {d}))) - (n |-> rr))) by FINSEQ_1:def 3;
A17: dom (F | (X \ {d})) = (dom F) /\ (X \ {d}) by RELAT_1:61;
A18: dom (F | X) = (dom F) /\ X by RELAT_1:61;
A19: 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 object ; :: according to TARSKI:def 3 :: thesis: ( not y in dom (F | (X \ {d})) or y in (dom (F | X)) \ {d} )
assume A20: y in dom (F | (X \ {d})) ; :: thesis: y in (dom (F | X)) \ {d}
then y in X \ {d} by A17, XBOOLE_0:def 4;
then A21: not y in {d} by XBOOLE_0:def 5;
y in dom F by A17, A20, XBOOLE_0:def 4;
then y in dom (F | X) by A17, A18, A20, XBOOLE_0:def 4;
hence y in (dom (F | X)) \ {d} by A21, XBOOLE_0:def 5; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (dom (F | X)) \ {d} or y in dom (F | (X \ {d})) )
assume A22: y in (dom (F | X)) \ {d} ; :: thesis: y in dom (F | (X \ {d}))
then A23: not y in {d} by XBOOLE_0:def 5;
A24: y in dom (F | X) by A22, XBOOLE_0:def 5;
then y in X by A18, XBOOLE_0:def 4;
then A25: y in X \ {d} by A23, XBOOLE_0:def 5;
y in dom F by A18, A24, XBOOLE_0:def 4;
hence y in dom (F | (X \ {d})) by A17, A25, XBOOLE_0:def 4; :: thesis: verum
end;
then reconsider dx = dom (F | X), dy = dom (F | (X \ {d})) as finite set by A3;
A26: card dy = (card dx) - (card {d}) by A12, A19, CARD_2:44
.= (n + 1) - 1 by A3, A8, CARD_1:30
.= n ;
then ( len (n |-> rr) = n & len (FinS (F,(X \ {d}))) = n ) by Th67, CARD_1:def 7;
then A27: len ((FinS (F,(X \ {d}))) - (n |-> rr)) = n by FINSEQ_2:72;
(F - r) . d = (FinS ((F - rr),X)) . (len (FinS ((F - rr),X))) by A10, A11, FUNCT_1:47;
then A28: FinS ((F - rr),X) = ((FinS ((F - rr),X)) | n) ^ <*((F - r) . d)*> by A8, A5, RFINSEQ:7;
(FinS ((F - r),(X \ {d}))) ^ <*((F - r) . d)*>,(F - r) | X are_fiberwise_equipotent by A3, A4, A10, Th66;
then (FinS ((F - r),(X \ {d}))) ^ <*((F - r) . d)*>, FinS ((F - rr),X) are_fiberwise_equipotent by A6, CLASSES1:76;
then ( (FinS ((F - rr),X)) | n is non-increasing & FinS ((F - r),(X \ {d})),(FinS ((F - rr),X)) | n are_fiberwise_equipotent ) by A28, RFINSEQ:1, RFINSEQ:20;
then A29: FinS ((F - r),(X \ {d})) = (FinS ((F - rr),X)) | n by RFINSEQ:23;
len ((n + 1) |-> rr) = n + 1 by CARD_1:def 7;
then A30: len ((FinS (F,X)) - ((n + 1) |-> rr)) = n + 1 by A9, FINSEQ_2:72;
then A31: dom ((FinS (F,X)) - ((n + 1) |-> rr)) = Seg (n + 1) by FINSEQ_1:def 3;
dom ((F - r) | X) = (dom (F - r)) /\ X by RELAT_1:61;
then d in dom (F - r) by A10, 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 A32: <*((F - r) . d)*> = <*(F . d)*> - <*r*> by RVSUM_1:29;
A33: n < n + 1 by NAT_1:13;
A34: dom (FinS (F,X)) = Seg (len (FinS (F,X))) by FINSEQ_1:def 3;
reconsider Fd = <*(F . d)*>, rr = <*r*> as FinSequence of REAL by RVSUM_1:145;
( len <*(F . d)*> = 1 & len <*r*> = 1 ) by FINSEQ_1:40;
then A35: len (Fd - rr) = 1 by FINSEQ_2:72;
then A36: len (((FinS (F,(X \ {d}))) - (n |-> rr)) ^ (<*(F . d)*> - <*r*>)) = n + 1 by A27, FINSEQ_1:22;
1 in Seg 1 by FINSEQ_1:1;
then A37: 1 in dom (<*(F . d)*> - <*r*>) by A35, FINSEQ_1:def 3;
A38: ( <*(F . d)*> . 1 = F . d & <*r*> . 1 = r ) ;
A39: now :: thesis: for m being Nat st m in dom ((FinS (F,X)) - ((n + 1) |-> rr)) holds
((FinS (F,X)) - ((n + 1) |-> rr)) . m = (((FinS (F,(X \ {d}))) - (n |-> rr)) ^ (<*(F . d)*> - <*r*>)) . m
let m be Nat; :: thesis: ( m in dom ((FinS (F,X)) - ((n + 1) |-> rr)) implies ((FinS (F,X)) - ((n + 1) |-> rr)) . b1 = (((FinS (F,(X \ {d}))) - (n |-> rr)) ^ (<*(F . d)*> - <*r*>)) . b1 )
assume A40: m in dom ((FinS (F,X)) - ((n + 1) |-> rr)) ; :: thesis: ((FinS (F,X)) - ((n + 1) |-> rr)) . b1 = (((FinS (F,(X \ {d}))) - (n |-> rr)) ^ (<*(F . d)*> - <*r*>)) . b1
per cases ( m = n + 1 or m <> n + 1 ) ;
suppose A41: m = n + 1 ; :: thesis: ((FinS (F,X)) - ((n + 1) |-> rr)) . b1 = (((FinS (F,(X \ {d}))) - (n |-> rr)) ^ (<*(F . d)*> - <*r*>)) . b1
then A42: ((n + 1) |-> rr) . m = r by FINSEQ_1:4, FUNCOP_1:7;
(((FinS (F,(X \ {d}))) - (n |-> rr)) ^ (<*(F . d)*> - <*r*>)) . m = (<*(F . d)*> - <*r*>) . ((n + 1) - n) by A27, A36, A33, A41, FINSEQ_1:24
.= (F . d) - r by A38, A37, VALUED_1:13 ;
hence ((FinS (F,X)) - ((n + 1) |-> rr)) . m = (((FinS (F,(X \ {d}))) - (n |-> rr)) ^ (<*(F . d)*> - <*r*>)) . m by A13, A9, A40, A41, A42, VALUED_1:13; :: thesis: verum
end;
suppose A43: m <> n + 1 ; :: thesis: (((FinS (F,(X \ {d}))) - (n |-> rr)) ^ (<*(F . d)*> - <*r*>)) . b1 = ((FinS (F,X)) - ((n + 1) |-> rr)) . b1
m <= n + 1 by A31, A40, FINSEQ_1:1;
then m < n + 1 by A43, XXREAL_0:1;
then A44: m <= n by NAT_1:13;
reconsider s = (FinS (F,X)) . m as Element of REAL by XREAL_0:def 1;
A45: n <= n + 1 by NAT_1:11;
A46: ((n + 1) |-> rr) . m = r by A31, A40, FUNCOP_1:7;
A47: 1 <= m by A31, A40, FINSEQ_1:1;
then A48: m in Seg n by A44, FINSEQ_1:1;
then A49: m in dom ((FinS (F,(X \ {d}))) - (n |-> rr)) by A27, FINSEQ_1:def 3;
1 <= n by A47, A44, XXREAL_0:2;
then n in Seg (n + 1) by A45, FINSEQ_1:1;
then A50: ((FinS (F,X)) | n) . m = (FinS (F,X)) . m by A9, A34, A48, RFINSEQ:6;
( (((FinS (F,(X \ {d}))) - (n |-> rr)) ^ (<*(F . d)*> - <*r*>)) . m = ((FinS (F,(X \ {d}))) - (n |-> rr)) . m & (n |-> rr) . m = r ) by A27, A16, A48, FINSEQ_1:def 7, FUNCOP_1:7;
hence (((FinS (F,(X \ {d}))) - (n |-> rr)) ^ (<*(F . d)*> - <*r*>)) . m = s - r by A15, A50, A49, VALUED_1:13
.= ((FinS (F,X)) - ((n + 1) |-> rr)) . m by A40, A46, VALUED_1:13 ;
:: thesis: verum
end;
end;
end;
FinS ((F - r),(X \ {d})) = (FinS (F,(X \ {d}))) - (n |-> rr) by A2, A26;
hence FinS ((F - r),X) = (FinS (F,X)) - ((card G) |-> r) by A8, A28, A29, A32, A30, A36, A39, FINSEQ_2:9; :: thesis: verum
end;
A51: 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 A52: 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 A53: dom (F | X) = {} by A52;
then FinS (F,X) = FinS (F,{}) by Th63
.= <*> REAL by Th68 ;
then A54: (FinS (F,X)) - ((card G) |-> rr) = <*> REAL by FINSEQ_2:73;
dom ((F - r) | X) = (dom (F - r)) /\ X by RELAT_1:61
.= (dom F) /\ X by VALUED_1:3
.= dom (F | X) by RELAT_1:61 ;
hence FinS ((F - r),X) = FinS ((F - r),{}) by A53, Th63
.= (FinS (F,X)) - ((card G) |-> r) by A54, Th68 ;
:: thesis: verum
end;
A55: for n being Nat holds S2[n] from NAT_1:sch 2(A51, A1);
 let G be finite set ; :: thesis: ( G = dom (F | X) implies FinS ((F - r),X) = (FinS (F,X)) - ((card G) |-> r) )
assume G = dom (F | X) ; :: thesis: FinS ((F - r),X) = (FinS (F,X)) - ((card G) |-> r)
hence FinS ((F - r),X) = (FinS (F,X)) - ((card G) |-> r) by A55; :: thesis: verum