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)
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);
A1: 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 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 - r),X;
set fx = FinS F,X;
A4: 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 A5: len (FinS (F - r),X) = card G by A3, Th70;
A6: FinS (F - r),X,(F - r) | X are_fiberwise_equipotent by A3, A4, Def14;
then A7: rng (FinS (F - r),X) = rng ((F - r) | X) by CLASSES1:83;
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, Th70;
0 + 1 <= n + 1 by NAT_1:13;
then len (FinS (F - r),X) in dom (FinS (F - r),X) by A8, A5, 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
A10: d in dom ((F - r) | X) and
A11: ((F - r) | X) . d = (FinS (F - r),X) . (len (FinS (F - r),X)) by A7, PARTFUN1:26;
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;
A12: {d} c= dom (F | X) by A4, A10, ZFMISC_1:37;
(F - r) . d = (FinS (F - r),X) . (len (FinS (F - r),X)) by A10, A11, FUNCT_1:70;
then A13: (FinS F,X) . (len (FinS F,X)) = F . d by A3, A4, A10, Th75;
len (FinS F,X) = card G by A3, Th70;
then A14: FinS F,X = ((FinS F,X) | n) ^ <*(F . d)*> by A8, A13, RFINSEQ:20;
FinS F,X = (FinS F,(X \ {d})) ^ <*(F . d)*> by A3, A4, A10, A13, Th73;
then A15: FinS F,(X \ {d}) = (FinS F,X) | n by A14, FINSEQ_1:46;
A16: dom ((FinS F,(X \ {d})) - (n |-> r)) = Seg (len ((FinS F,(X \ {d})) - (n |-> r))) by FINSEQ_1:def 3;
A17: dom (F | (X \ {d})) = (dom F) /\ (X \ {d}) by RELAT_1:90;
A18: dom (F | X) = (dom F) /\ X by RELAT_1:90;
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 set ; :: 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 set ; :: 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:63
.= (n + 1) - 1 by A3, A8, CARD_1:50
.= n ;
then ( len (n |-> r) = n & len (FinS F,(X \ {d})) = n ) by Th70, FINSEQ_1:def 18;
then A27: len ((FinS F,(X \ {d})) - (n |-> r)) = n by FINSEQ_2:86;
(F - r) . d = (FinS (F - r),X) . (len (FinS (F - r),X)) by A10, A11, FUNCT_1:70;
then A28: FinS (F - r),X = ((FinS (F - r),X) | n) ^ <*((F - r) . d)*> by A8, A5, RFINSEQ:20;
(FinS (F - r),(X \ {d})) ^ <*((F - r) . d)*>,(F - r) | X are_fiberwise_equipotent by A3, A4, A10, Th69;
then (FinS (F - r),(X \ {d})) ^ <*((F - r) . d)*>, FinS (F - r),X are_fiberwise_equipotent by A6, CLASSES1:84;
then ( (FinS (F - r),X) | n is non-increasing & FinS (F - r),(X \ {d}),(FinS (F - r),X) | n are_fiberwise_equipotent ) by A28, RFINSEQ:14, RFINSEQ:33;
then A29: FinS (F - r),(X \ {d}) = (FinS (F - r),X) | n by RFINSEQ:36;
len ((n + 1) |-> r) = n + 1 by FINSEQ_1:def 18;
then A30: len ((FinS F,X) - ((n + 1) |-> r)) = n + 1 by A9, FINSEQ_2:86;
then A31: dom ((FinS F,X) - ((n + 1) |-> r)) = Seg (n + 1) by FINSEQ_1:def 3;
dom ((F - r) | X) = (dom (F - r)) /\ X by RELAT_1:90;
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:50;
A33: n < n + 1 by NAT_1:13;
A34: dom (FinS F,X) = Seg (len (FinS F,X)) by FINSEQ_1:def 3;
( len <*(F . d)*> = 1 & len <*r*> = 1 ) 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 A27, FINSEQ_1:35;
1 in Seg 1 by FINSEQ_1:3;
then A37: 1 in dom (<*(F . d)*> - <*r*>) by A35, FINSEQ_1:def 3;
A38: ( <*(F . d)*> . 1 = F . d & <*r*> . 1 = r ) by FINSEQ_1:57;
A39: 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 A40: 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 A41: m = n + 1 ; :: thesis: ((FinS F,X) - ((n + 1) |-> r)) . b1 = (((FinS F,(X \ {d})) - (n |-> r)) ^ (<*(F . d)*> - <*r*>)) . b1
then A42: ((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 A27, A36, A33, A41, FINSEQ_1:37
.= (F . d) - r by A38, A37, VALUED_1:13 ;
hence ((FinS F,X) - ((n + 1) |-> r)) . m = (((FinS F,(X \ {d})) - (n |-> r)) ^ (<*(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 |-> r)) ^ (<*(F . d)*> - <*r*>)) . b1 = ((FinS F,X) - ((n + 1) |-> r)) . b1
m <= n + 1 by A31, A40, FINSEQ_1:3;
then m < n + 1 by A43, XXREAL_0:1;
then A44: m <= n by NAT_1:13;
reconsider s = (FinS F,X) . m as Real ;
A45: n <= n + 1 by NAT_1:11;
A46: ((n + 1) |-> r) . m = r by A31, A40, FUNCOP_1:13;
A47: 1 <= m by A31, A40, FINSEQ_1:3;
then A48: m in Seg n by A44, FINSEQ_1:3;
then A49: m in dom ((FinS F,(X \ {d})) - (n |-> r)) by A27, FINSEQ_1:def 3;
1 <= n by A47, A44, XXREAL_0:2;
then n in Seg (n + 1) by A45, FINSEQ_1:3;
then A50: ((FinS F,X) | n) . m = (FinS F,X) . m by A9, A34, A48, RFINSEQ:19;
( (((FinS F,(X \ {d})) - (n |-> r)) ^ (<*(F . d)*> - <*r*>)) . m = ((FinS F,(X \ {d})) - (n |-> r)) . m & (n |-> r) . m = r ) by A27, A16, A48, FINSEQ_1:def 7, FUNCOP_1:13;
hence (((FinS F,(X \ {d})) - (n |-> r)) ^ (<*(F . d)*> - <*r*>)) . m = s - r by A15, A50, A49, VALUED_1:13
.= ((FinS F,X) - ((n + 1) |-> r)) . m by A40, A46, VALUED_1:13 ;
:: thesis: verum
end;
end;
end;
FinS (F - r),(X \ {d}) = (FinS F,(X \ {d})) - (n |-> r) by A2, A26;
hence FinS (F - r),X = (FinS F,X) - ((card G) |-> r) by A8, A28, A29, A32, A30, A36, A39, FINSEQ_2:10; :: 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 Th66
.= <*> REAL by Th71 ;
then A54: (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 A53, Th66
.= (FinS F,X) - ((card G) |-> r) by A54, Th71 ;
:: thesis: verum
end;
A55: for n being Element of NAT holds S2[n] from NAT_1:sch 1(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