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

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

MIM R = ((MIM R) | n) ^ <*(r - s),s*>

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

MIM R = ((MIM R) | n) ^ <*(r - s),s*>

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

set mf = MIM R;

set nf = (MIM R) | n;

assume that

A1: len R = n + 2 and

A2: R . (n + 1) = r and

A3: R . (n + 2) = s ; :: thesis: MIM R = ((MIM R) | n) ^ <*(r - s),s*>

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

then A5: dom (MIM R) = Seg (n + 2) by FINSEQ_1:def 3;

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

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

then A7: n < n + 2 by NAT_1:13;

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

then len (((MIM R) | n) ^ <*(r - s),s*>) = n + (len <*(r - s),s*>) by FINSEQ_1:22;

then A9: len (((MIM R) | n) ^ <*(r - s),s*>) = n + 2 by FINSEQ_1:44;

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

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

MIM R = ((MIM R) | n) ^ <*(r - s),s*>

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

MIM R = ((MIM R) | n) ^ <*(r - s),s*>

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

set mf = MIM R;

set nf = (MIM R) | n;

assume that

A1: len R = n + 2 and

A2: R . (n + 1) = r and

A3: R . (n + 2) = s ; :: thesis: MIM R = ((MIM R) | n) ^ <*(r - s),s*>

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

then A5: dom (MIM R) = Seg (n + 2) by FINSEQ_1:def 3;

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

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

then A7: n < n + 2 by NAT_1:13;

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

then len (((MIM R) | n) ^ <*(r - s),s*>) = n + (len <*(r - s),s*>) by FINSEQ_1:22;

then A9: len (((MIM R) | n) ^ <*(r - s),s*>) = n + 2 by FINSEQ_1:44;

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

now :: thesis: for m being Nat st m in dom (MIM R) holds

(MIM R) . m = (((MIM R) | n) ^ <*(r - s),s*>) . m

hence
MIM R = ((MIM R) | n) ^ <*(r - s),s*>
by A4, A9, FINSEQ_2:9; :: thesis: verum(MIM R) . m = (((MIM R) | n) ^ <*(r - s),s*>) . m

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

assume A11: m in dom (MIM R) ; :: thesis: (MIM R) . m = (((MIM R) | n) ^ <*(r - s),s*>) . m

then A12: 1 <= m by A5, FINSEQ_1:1;

A13: m <= n + 2 by A5, A11, FINSEQ_1:1;

end;assume A11: m in dom (MIM R) ; :: thesis: (MIM R) . m = (((MIM R) | n) ^ <*(r - s),s*>) . m

then A12: 1 <= m by A5, FINSEQ_1:1;

A13: m <= n + 2 by A5, A11, FINSEQ_1:1;

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

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

end;

case A14:
m = n + 2
; :: thesis: (MIM R) . m = (((MIM R) | n) ^ <*(r - s),s*>) . m

hence (MIM R) . m =
s
by A1, A3, A4, Def2

.= <*(r - s),s*> . ((n + 2) - n) by FINSEQ_1:44

.= (((MIM R) | n) ^ <*(r - s),s*>) . m by A8, A9, A7, A14, FINSEQ_1:24 ;

:: thesis: verum

end;.= <*(r - s),s*> . ((n + 2) - n) by FINSEQ_1:44

.= (((MIM R) | n) ^ <*(r - s),s*>) . m by A8, A9, A7, A14, FINSEQ_1:24 ;

:: thesis: verum

case
m <> n + 2
; :: thesis: (MIM R) . m = (((MIM R) | n) ^ <*(r - s),s*>) . m

then
m < n + 2
by A13, XXREAL_0:1;

then A15: m <= n + 1 by A6, NAT_1:13;

A16: (len (MIM R)) - 1 = n + 1 by A4;

end;then A15: m <= n + 1 by A6, NAT_1:13;

A16: (len (MIM R)) - 1 = n + 1 by A4;

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

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

end;

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

then A18:
n < m
by NAT_1:13;

thus (MIM R) . m = r - s by A2, A3, A6, A12, A16, A17, Def2

.= <*(r - s),s*> . ((n + 1) - n) by FINSEQ_1:44

.= (((MIM R) | n) ^ <*(r - s),s*>) . m by A8, A9, A13, A17, A18, FINSEQ_1:24 ; :: thesis: verum

end;thus (MIM R) . m = r - s by A2, A3, A6, A12, A16, A17, Def2

.= <*(r - s),s*> . ((n + 1) - n) by FINSEQ_1:44

.= (((MIM R) | n) ^ <*(r - s),s*>) . m by A8, A9, A13, A17, A18, FINSEQ_1:24 ; :: thesis: verum

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

then
m < n + 1
by A15, XXREAL_0:1;

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

then A20: m in Seg n by A12, FINSEQ_1:1;

1 <= n by A12, A19, XXREAL_0:2;

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

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

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

hence (MIM R) . m = ((MIM R) | n) . m by A4, A20, A21, Th6

.= (((MIM R) | n) ^ <*(r - s),s*>) . m by A8, A20, A22, FINSEQ_1:def 7 ;

:: thesis: verum

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

then A20: m in Seg n by A12, FINSEQ_1:1;

1 <= n by A12, A19, XXREAL_0:2;

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

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

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

hence (MIM R) . m = ((MIM R) | n) . m by A4, A20, A21, Th6

.= (((MIM R) | n) ^ <*(r - s),s*>) . m by A8, A20, A22, FINSEQ_1:def 7 ;

:: thesis: verum