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:25;
A3: i <= len w by A1, FINSEQ_3:25;
A4: len (((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) = (len ((w | (i -' 1)) ^ <*r*>)) + (len (w /^ i)) by FINSEQ_1:22
.= ((len (w | (i -' 1))) + (len <*r*>)) + (len (w /^ i)) by FINSEQ_1:22
.= ((len (w | (i -' 1))) + 1) + (len (w /^ i)) by FINSEQ_1:39
.= ((i -' 1) + 1) + (len (w /^ i)) by A3, FINSEQ_1:59, NAT_D:44
.= ((i -' 1) + 1) + ((len w) - i) by A3, RFINSEQ:def 1
.= ((i - 1) + 1) + ((len w) - i) by A2, XREAL_1:233 ;
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:59, NAT_D:44
.= i - 1 by A2, XREAL_1:233 ;
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:22
.= (len (w | (i -' 1))) + 1 by FINSEQ_1:39
.= (i -' 1) + 1 by A3, FINSEQ_1:59, NAT_D:44
.= (i - 1) + 1 by A2, XREAL_1:233
.= i ;
A9: len (w +* (i,r)) = len w by Th96;

now :: thesis: ( ( i < j & (w +* (i,r)) . j = (((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) . j ) or ( j = i & (w +* (i,r)) . j = (((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) . j ) or ( j < i & (w +* (i,r)) . j = (((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) . j ) )

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:9;
then A12: 1 <= j -' i by NAT_D:39;
A13: j - i <= (len w) - i by A7, A9, XREAL_1:9;
A14: i <= len w by A1, FINSEQ_3:25;
len (w /^ i) = (len w) -' i by RFINSEQ:29
.= (len w) - i by A14, XREAL_1:233 ;
then j -' i <= len (w /^ i) by A11, A13, NAT_D:39;
then A15: j -' i in dom (w /^ i) by A12, FINSEQ_3:25;
j <= len (((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) by A4, A7, Th96;
then (((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) . j = (w /^ i) . (j - (len ((w | (i -' 1)) ^ <*r*>))) by A8, A10, FINSEQ_1:24
.= (w /^ i) . (j -' i) by A8, A10, XREAL_1:233
.= w . ((j -' i) + i) by A14, A15, RFINSEQ:def 1
.= w . j by A10, XREAL_1:235 ;
hence (w +* (i,r)) . j = (((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) . j by A10, Th31; :: 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:64
.= r by A17, FINSEQ_1:42 ;
hence (w +* (i,r)) . j = (((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) . j by A1, A16, Th30; :: 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:9;
then A20: j <= i -' 1 by A2, XREAL_1:233;
(((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) . j = ((w | (i -' 1)) ^ <*r*>) . j by A6, A8, A18, FINSEQ_1:64
.= (w | (i -' 1)) . j by A6, A5, A19, FINSEQ_1:64
.= w . j by A20, FINSEQ_3:112 ;
hence (w +* (i,r)) . j = (((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) . j by A18, Th31; :: 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, Th96, FINSEQ_1:14; :: thesis: verum