let i be Nat; :: thesis: for D being non empty set
for w being FinSequence of D
for r being Element of D st i in dom w holds
w +* i,r = ((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)
let D be non empty set ; :: thesis: for w being FinSequence of D
for r being Element of D st i in dom w holds
w +* i,r = ((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)
let w be FinSequence of D; :: thesis: for r being Element of D st i in dom w holds
w +* i,r = ((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)
let r be Element of D; :: thesis: ( i in dom w implies w +* i,r = ((w | (i -' 1)) ^ <*r*>) ^ (w /^ i) )
assume A1: i in dom w ; :: thesis: w +* i,r = ((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)
then A2: 1 <= i by FINSEQ_3:27;
A3: i <= len w by A1, FINSEQ_3:27;
A4: len (((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) = (len ((w | (i -' 1)) ^ <*r*>)) + (len (w /^ i)) by FINSEQ_1:35
.= ((len (w | (i -' 1))) + (len <*r*>)) + (len (w /^ i)) by FINSEQ_1:35
.= ((len (w | (i -' 1))) + 1) + (len (w /^ i)) by FINSEQ_1:56
.= ((i -' 1) + 1) + (len (w /^ i)) by A3, FINSEQ_1:80, NAT_D:44
.= ((i -' 1) + 1) + ((len w) - i) by A3, RFINSEQ:def 2
.= ((i - 1) + 1) + ((len w) - i) by A2, XREAL_1:235 ;
for j being Nat st 1 <= j & j <= len (w +* i,r) holds
(w +* i,r) . j = (((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) . j

proof

A5: len (w | (i -' 1)) = i -' 1 by A3, FINSEQ_1:80, NAT_D:44
.= i - 1 by A2, XREAL_1:235 ;
let j be Nat; :: thesis: ( 1 <= j & j <= len (w +* i,r) implies (w +* i,r) . j = (((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) . j )
assume that
A6: 1 <= j and
A7: j <= len (w +* i,r) ; :: thesis: (w +* i,r) . j = (((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) . j
A8: len ((w | (i -' 1)) ^ <*r*>) = (len (w | (i -' 1))) + (len <*r*>) by FINSEQ_1:35
.= (len (w | (i -' 1))) + 1 by FINSEQ_1:56
.= (i -' 1) + 1 by A3, FINSEQ_1:80, NAT_D:44
.= (i - 1) + 1 by A2, XREAL_1:235
.= i ;
A9: len (w +* i,r) = len w by Th99;

now

per cases ( i < j or j = i or j < i ) by XXREAL_0:1;

case A10: i < j ; :: thesis: (w +* i,r) . j = (((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) . j

then i + 1 <= j by NAT_1:13;
then A11: (i + 1) - i <= j - i by XREAL_1:11;
then A12: 1 <= j -' i by NAT_D:39;
A13: j - i <= (len w) - i by A7, A9, XREAL_1:11;
A14: i <= len w by A1, FINSEQ_3:27;
len (w /^ i) = (len w) -' i by RFINSEQ:42
.= (len w) - i by A14, XREAL_1:235 ;
then j -' i <= len (w /^ i) by A11, A13, NAT_D:39;
then A15: j -' i in dom (w /^ i) by A12, FINSEQ_3:27;
j <= len (((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) by A4, A7, Th99;
then (((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) . j = (w /^ i) . (j - (len ((w | (i -' 1)) ^ <*r*>))) by A8, A10, FINSEQ_1:37
.= (w /^ i) . (j -' i) by A8, A10, XREAL_1:235
.= w . ((j -' i) + i) by A14, A15, RFINSEQ:def 2
.= w . j by A10, XREAL_1:237 ;
hence (w +* i,r) . j = (((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) . j by A10, Th34; :: thesis: verum

end;

case A16: j = i ; :: thesis: (w +* i,r) . j = (((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) . j

A17: i = (len (w | (i -' 1))) + 1 by A5;
(((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) . j = ((w | (i -' 1)) ^ <*r*>) . i by A6, A8, A16, FINSEQ_1:85
.= r by A17, FINSEQ_1:59 ;
hence (w +* i,r) . j = (((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) . j by A1, A16, Th33; :: thesis: verum

end;

case A18: j < i ; :: thesis: (w +* i,r) . j = (((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) . j

then j + 1 <= i by NAT_1:13;
then A19: (j + 1) - 1 <= i - 1 by XREAL_1:11;
then A20: j <= i -' 1 by A2, XREAL_1:235;
(((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) . j = ((w | (i -' 1)) ^ <*r*>) . j by A6, A8, A18, FINSEQ_1:85
.= (w | (i -' 1)) . j by A6, A5, A19, FINSEQ_1:85
.= w . j by A20, FINSEQ_3:121 ;
hence (w +* i,r) . j = (((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) . j by A18, Th34; :: thesis: verum

end;

end;

end;

hence (w +* i,r) . j = (((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) . j ; :: thesis: verum

end;

hence w +* i,r = ((w | (i -' 1)) ^ <*r*>) ^ (w /^ i) by A4, Th99, FINSEQ_1:18; :: thesis: verum