let R be FinSequence of REAL ; :: thesis: for r being Real

for n being Nat st len R = n + 2 & R . (n + 1) = r holds

MIM (R | (n + 1)) = ((MIM R) | n) ^ <*r*>

let s be Real; :: thesis: for n being Nat st len R = n + 2 & R . (n + 1) = s holds

MIM (R | (n + 1)) = ((MIM R) | n) ^ <*s*>

let n be Nat; :: thesis: ( len R = n + 2 & R . (n + 1) = s implies MIM (R | (n + 1)) = ((MIM R) | n) ^ <*s*> )

assume that

A1: len R = n + 2 and

A2: R . (n + 1) = s ; :: thesis: MIM (R | (n + 1)) = ((MIM R) | n) ^ <*s*>

set f1 = R | (n + 1);

set m1 = MIM (R | (n + 1));

set mf = MIM R;

set fn = (MIM R) | n;

A3: 0 + 1 <= n + 1 by NAT_1:13;

A4: (n + 1) + 1 = n + (1 + 1) ;

then n + 1 <= n + 2 by NAT_1:11;

then A5: ( Seg (len R) = dom R & n + 1 in Seg (n + 2) ) by A3, FINSEQ_1:1, FINSEQ_1:def 3;

A6: len (R | (n + 1)) = n + 1 by A1, A4, FINSEQ_1:59, NAT_1:11;

then A7: len (MIM (R | (n + 1))) = n + 1 by Def2;

then A8: dom (MIM (R | (n + 1))) = Seg (n + 1) by FINSEQ_1:def 3;

n + 1 in Seg (n + 1) by A3, FINSEQ_1:1;

then (R | (n + 1)) . (n + 1) = s by A1, A2, A5, Th6;

then A9: (MIM (R | (n + 1))) . (n + 1) = s by A6, A7, Def2;

A10: Seg (len ((MIM R) | n)) = dom ((MIM R) | n) by FINSEQ_1:def 3;

A11: Seg (len (MIM R)) = dom (MIM R) by FINSEQ_1:def 3;

A12: len (MIM R) = n + 2 by A1, Def2;

then A13: len ((MIM R) | n) = n by FINSEQ_1:59, NAT_1:11;

A14: n <= n + 2 by NAT_1:11;

.= n + 1 by FINSEQ_1:40 ;

hence MIM (R | (n + 1)) = ((MIM R) | n) ^ <*s*> by A7, A15, FINSEQ_2:9; :: thesis: verum

for n being Nat st len R = n + 2 & R . (n + 1) = r holds

MIM (R | (n + 1)) = ((MIM R) | n) ^ <*r*>

let s be Real; :: thesis: for n being Nat st len R = n + 2 & R . (n + 1) = s holds

MIM (R | (n + 1)) = ((MIM R) | n) ^ <*s*>

let n be Nat; :: thesis: ( len R = n + 2 & R . (n + 1) = s implies MIM (R | (n + 1)) = ((MIM R) | n) ^ <*s*> )

assume that

A1: len R = n + 2 and

A2: R . (n + 1) = s ; :: thesis: MIM (R | (n + 1)) = ((MIM R) | n) ^ <*s*>

set f1 = R | (n + 1);

set m1 = MIM (R | (n + 1));

set mf = MIM R;

set fn = (MIM R) | n;

A3: 0 + 1 <= n + 1 by NAT_1:13;

A4: (n + 1) + 1 = n + (1 + 1) ;

then n + 1 <= n + 2 by NAT_1:11;

then A5: ( Seg (len R) = dom R & n + 1 in Seg (n + 2) ) by A3, FINSEQ_1:1, FINSEQ_1:def 3;

A6: len (R | (n + 1)) = n + 1 by A1, A4, FINSEQ_1:59, NAT_1:11;

then A7: len (MIM (R | (n + 1))) = n + 1 by Def2;

then A8: dom (MIM (R | (n + 1))) = Seg (n + 1) by FINSEQ_1:def 3;

n + 1 in Seg (n + 1) by A3, FINSEQ_1:1;

then (R | (n + 1)) . (n + 1) = s by A1, A2, A5, Th6;

then A9: (MIM (R | (n + 1))) . (n + 1) = s by A6, A7, Def2;

A10: Seg (len ((MIM R) | n)) = dom ((MIM R) | n) by FINSEQ_1:def 3;

A11: Seg (len (MIM R)) = dom (MIM R) by FINSEQ_1:def 3;

A12: len (MIM R) = n + 2 by A1, Def2;

then A13: len ((MIM R) | n) = n by FINSEQ_1:59, NAT_1:11;

A14: n <= n + 2 by NAT_1:11;

A15: now :: thesis: for m being Nat st m in dom (MIM (R | (n + 1))) holds

(MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m

len (((MIM R) | n) ^ <*s*>) =
n + (len <*s*>)
by A13, FINSEQ_1:22
(MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m

let m be Nat; :: thesis: ( m in dom (MIM (R | (n + 1))) implies (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m )

assume A16: m in dom (MIM (R | (n + 1))) ; :: thesis: (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m

then A17: 1 <= m by A8, FINSEQ_1:1;

A18: m <= n + 1 by A8, A16, FINSEQ_1:1;

end;assume A16: m in dom (MIM (R | (n + 1))) ; :: thesis: (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m

then A17: 1 <= m by A8, FINSEQ_1:1;

A18: m <= n + 1 by A8, A16, FINSEQ_1:1;

now :: thesis: ( ( m = n + 1 & (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m ) or ( m <> n + 1 & (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m ) )end;

hence
(MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m
; :: thesis: verumper cases
( m = n + 1 or m <> n + 1 )
;

end;

case
m = n + 1
; :: thesis: (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m

hence
(MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m
by A13, A9, FINSEQ_1:42; :: thesis: verum

end;case
m <> n + 1
; :: thesis: (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m

then A19:
m < n + 1
by A18, XXREAL_0:1;

then A20: m <= n by NAT_1:13;

then A21: m in Seg n by A17, FINSEQ_1:1;

set r2 = R . (m + 1);

set r1 = R . m;

A22: (len (MIM R)) - 1 = n + 1 by A12;

1 <= n by A17, A20, XXREAL_0:2;

then n in Seg (n + 2) by A14, FINSEQ_1:1;

then ((MIM R) | n) . m = (MIM R) . m by A12, A11, A21, Th6;

then A23: (R . m) - (R . (m + 1)) = ((MIM R) | n) . m by A17, A18, A22, Def2

.= (((MIM R) | n) ^ <*s*>) . m by A13, A10, A21, FINSEQ_1:def 7 ;

( 1 <= m + 1 & m + 1 <= n + 1 ) by A19, NAT_1:11, NAT_1:13;

then m + 1 in Seg (n + 1) by FINSEQ_1:1;

then A24: (R | (n + 1)) . (m + 1) = R . (m + 1) by A1, A5, Th6;

( (len (MIM (R | (n + 1)))) - 1 = n & (R | (n + 1)) . m = R . m ) by A1, A7, A5, A8, A16, Th6;

hence (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m by A17, A20, A23, A24, Def2; :: thesis: verum

end;then A20: m <= n by NAT_1:13;

then A21: m in Seg n by A17, FINSEQ_1:1;

set r2 = R . (m + 1);

set r1 = R . m;

A22: (len (MIM R)) - 1 = n + 1 by A12;

1 <= n by A17, A20, XXREAL_0:2;

then n in Seg (n + 2) by A14, FINSEQ_1:1;

then ((MIM R) | n) . m = (MIM R) . m by A12, A11, A21, Th6;

then A23: (R . m) - (R . (m + 1)) = ((MIM R) | n) . m by A17, A18, A22, Def2

.= (((MIM R) | n) ^ <*s*>) . m by A13, A10, A21, FINSEQ_1:def 7 ;

( 1 <= m + 1 & m + 1 <= n + 1 ) by A19, NAT_1:11, NAT_1:13;

then m + 1 in Seg (n + 1) by FINSEQ_1:1;

then A24: (R | (n + 1)) . (m + 1) = R . (m + 1) by A1, A5, Th6;

( (len (MIM (R | (n + 1)))) - 1 = n & (R | (n + 1)) . m = R . m ) by A1, A7, A5, A8, A16, Th6;

hence (MIM (R | (n + 1))) . m = (((MIM R) | n) ^ <*s*>) . m by A17, A20, A23, A24, Def2; :: thesis: verum

.= n + 1 by FINSEQ_1:40 ;

hence MIM (R | (n + 1)) = ((MIM R) | n) ^ <*s*> by A7, A15, FINSEQ_2:9; :: thesis: verum