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 & i <= len w ) by 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 A2, FINSEQ_1:80, NAT_D:44
.= ((i -' 1) + 1) + ((len w) - i) by A2, 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

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 A5: ( 1 <= j & j <= len (w +* i,r) ) ; :: thesis: (w +* i,r) . j = (((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) . j
A6: len (w +* i,r) = len w by Th99;
A7: 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 A2, FINSEQ_1:80, NAT_D:44
.= (i - 1) + 1 by A2, XREAL_1:235
.= i ;
A8: len (w | (i -' 1)) = i -' 1 by A2, FINSEQ_1:80, NAT_D:44
.= i - 1 by A2, XREAL_1:235 ;

now

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

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

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

end;

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

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

end;

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

then j + 1 <= i by NAT_1:13;
then A18: (j + 1) - 1 <= i - 1 by XREAL_1:11;
then A19: j <= i -' 1 by A2, XREAL_1:235;
(((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) . j = ((w | (i -' 1)) ^ <*r*>) . j by A5, A7, A17, FINSEQ_1:85
.= (w | (i -' 1)) . j by A5, A8, A18, FINSEQ_1:85
.= w . j by A19, FINSEQ_3:121 ;
hence (w +* i,r) . j = (((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) . j by A17, 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 Th99, A4, FINSEQ_1:18; :: thesis: verum