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;
p c= Seg (len a) by A32, FINSEQ_1:def 3;
then a35: p is included_in_Seg ;
i in Seg i by A34;
then {i} c= Seg i by ZFMISC_1:31;
then a36: {i} is included_in_Seg ;
A40: for m, n being Nat st m in p & n in {i} holds
m < n

proof

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;

A41: for z being object holds not z in p /\ {i}

proof

let z be object ; :: thesis: not z in p /\ {i}

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

assume 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;

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

end;

A50: Sgm (p \/ {i}) = (Sgm p) ^ (Sgm {i}) by a35, a36, A40, FINSEQ_3:42
.= (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 14;
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