let a be non empty FinSequence of REAL ; :: thesis: for p being set

for i being Nat st p \/ {i} c= dom a & ( for m being Nat st m in p holds

m < i ) holds

Seq (a | (p \/ {i})) = (Seq (a | p)) ^ <*(a . i)*>

let p be set ; :: thesis: for i being Nat st p \/ {i} c= dom a & ( for m being Nat st m in p holds

m < i ) holds

Seq (a | (p \/ {i})) = (Seq (a | p)) ^ <*(a . i)*>

let i be Nat; :: thesis: ( p \/ {i} c= dom a & ( for m being Nat st m in p holds

m < i ) implies Seq (a | (p \/ {i})) = (Seq (a | p)) ^ <*(a . i)*> )

assume that

A00: p \/ {i} c= dom a and

A05: for m being Nat st m in p holds

m < i ; :: thesis: Seq (a | (p \/ {i})) = (Seq (a | p)) ^ <*(a . i)*>

A20: dom (a | (p \/ {i})) = p \/ {i} by A00, RELAT_1:62;

reconsider api = a | (p \/ {i}) as FinSubsequence ;

A32: p c= dom a by A00, XBOOLE_1:11;

i in dom a by A00, XBOOLE_1:11, ZFMISC_1:31;

then A34: ( 1 <= i & i <= len a ) by FINSEQ_3:25;

A35: p c= Seg (len a) by A32, FINSEQ_1:def 3;

i in Seg i by A34;

then A36: {i} c= Seg i by ZFMISC_1:31;

A40: for m, n being Nat st m in p & n in {i} holds

m < n

.= (Sgm p) ^ <*i*> by A34, FINSEQ_3:44 ;

set sgmp = Sgm p;

set poi = p \/ {i};

i in {i} by ZFMISC_1:31;

then reconsider i = i as Element of p \/ {i} by XBOOLE_0:def 3;

A57: rng (Sgm p) = p by A35, FINSEQ_1:def 13;

reconsider sgmp = Sgm p as FinSequence of p \/ {i} by XBOOLE_1:7, A57, FINSEQ_1:def 4;

A58: rng a c= REAL ;

rng api c= rng a by RELAT_1:70;

then rng api c= REAL by A58;

then reconsider api = api as Function of (p \/ {i}),REAL by A20, FUNCT_2:2;

A60: (a | (p \/ {i})) * (Sgm (p \/ {i})) = (api * sgmp) ^ <*(api . i)*> by A50, FINSEQOP:8;

A65: api = (a | p) \/ (a | {i}) by RELAT_1:78;

reconsider api = api as PartFunc of NAT,REAL ;

set apai = (a | p) \/ (a | {i});

A70: api * (Sgm p) = ((a | p) * (Sgm p)) \/ ((a | {i}) * (Sgm p)) by A65, RELAT_1:32;

A75: dom (a | p) = p by A00, XBOOLE_1:11, RELAT_1:62;

A82: p misses {i} by A41, XBOOLE_0:def 1;

dom (a | {i}) = {i} by A00, XBOOLE_1:11, RELAT_1:62;

then (a | {i}) * (Sgm p) = {} by A57, A82, RELAT_1:44;

hence Seq (a | (p \/ {i})) = (Seq (a | p)) ^ <*(a . i)*> by A20, A60, A70, A75, FUNCT_1:49; :: thesis: verum

for i being Nat st p \/ {i} c= dom a & ( for m being Nat st m in p holds

m < i ) holds

Seq (a | (p \/ {i})) = (Seq (a | p)) ^ <*(a . i)*>

let p be set ; :: thesis: for i being Nat st p \/ {i} c= dom a & ( for m being Nat st m in p holds

m < i ) holds

Seq (a | (p \/ {i})) = (Seq (a | p)) ^ <*(a . i)*>

let i be Nat; :: thesis: ( p \/ {i} c= dom a & ( for m being Nat st m in p holds

m < i ) implies Seq (a | (p \/ {i})) = (Seq (a | p)) ^ <*(a . i)*> )

assume that

A00: p \/ {i} c= dom a and

A05: for m being Nat st m in p holds

m < i ; :: thesis: Seq (a | (p \/ {i})) = (Seq (a | p)) ^ <*(a . i)*>

A20: dom (a | (p \/ {i})) = p \/ {i} by A00, RELAT_1:62;

reconsider api = a | (p \/ {i}) as FinSubsequence ;

A32: p c= dom a by A00, XBOOLE_1:11;

i in dom a by A00, XBOOLE_1:11, ZFMISC_1:31;

then A34: ( 1 <= i & i <= len a ) by FINSEQ_3:25;

A35: p c= Seg (len a) by A32, FINSEQ_1:def 3;

i in Seg i by A34;

then A36: {i} c= Seg i by ZFMISC_1:31;

A40: for m, n being Nat st m in p & n in {i} holds

m < n

proof

A41:
for z being object holds not z in p /\ {i}
let m, n be Nat; :: thesis: ( m in p & n in {i} implies m < n )

assume that

B00: m in p and

B10: n in {i} ; :: thesis: m < n

n = i by B10, TARSKI:def 1;

hence m < n by B00, A05; :: thesis: verum

end;assume that

B00: m in p and

B10: n in {i} ; :: thesis: m < n

n = i by B10, TARSKI:def 1;

hence m < n by B00, A05; :: thesis: verum

proof

A50: Sgm (p \/ {i}) =
(Sgm p) ^ (Sgm {i})
by A35, A36, A40, FINSEQ_3:42
let z be object ; :: thesis: not z in p /\ {i}

end;now :: thesis: not z in p /\ {i}

hence
not z in p /\ {i}
; :: thesis: verumassume
z in p /\ {i}
; :: thesis: contradiction

then C10: ( z in p & z in {i} ) by XBOOLE_0:def 4;

then z = i by TARSKI:def 1;

hence contradiction by C10, A05; :: thesis: verum

end;then C10: ( z in p & z in {i} ) by XBOOLE_0:def 4;

then z = i by TARSKI:def 1;

hence contradiction by C10, A05; :: thesis: verum

.= (Sgm p) ^ <*i*> by A34, FINSEQ_3:44 ;

set sgmp = Sgm p;

set poi = p \/ {i};

i in {i} by ZFMISC_1:31;

then reconsider i = i as Element of p \/ {i} by XBOOLE_0:def 3;

A57: rng (Sgm p) = p by A35, FINSEQ_1:def 13;

reconsider sgmp = Sgm p as FinSequence of p \/ {i} by XBOOLE_1:7, A57, FINSEQ_1:def 4;

A58: rng a c= REAL ;

rng api c= rng a by RELAT_1:70;

then rng api c= REAL by A58;

then reconsider api = api as Function of (p \/ {i}),REAL by A20, FUNCT_2:2;

A60: (a | (p \/ {i})) * (Sgm (p \/ {i})) = (api * sgmp) ^ <*(api . i)*> by A50, FINSEQOP:8;

A65: api = (a | p) \/ (a | {i}) by RELAT_1:78;

reconsider api = api as PartFunc of NAT,REAL ;

set apai = (a | p) \/ (a | {i});

A70: api * (Sgm p) = ((a | p) * (Sgm p)) \/ ((a | {i}) * (Sgm p)) by A65, RELAT_1:32;

A75: dom (a | p) = p by A00, XBOOLE_1:11, RELAT_1:62;

A82: p misses {i} by A41, XBOOLE_0:def 1;

dom (a | {i}) = {i} by A00, XBOOLE_1:11, RELAT_1:62;

then (a | {i}) * (Sgm p) = {} by A57, A82, RELAT_1:44;

hence Seq (a | (p \/ {i})) = (Seq (a | p)) ^ <*(a . i)*> by A20, A60, A70, A75, FUNCT_1:49; :: thesis: verum