let L be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for f being FinSequence of L
for i, j being Element of NAT st i in dom f & j = i - 1 holds
Ins ((Del (f,i)),j,(f /. i)) = f
let f be FinSequence of L; :: thesis: for i, j being Element of NAT st i in dom f & j = i - 1 holds
Ins ((Del (f,i)),j,(f /. i)) = f
let i, j be Element of NAT ; :: thesis: ( i in dom f & j = i - 1 implies Ins ((Del (f,i)),j,(f /. i)) = f )
set g = Ins ((Del (f,i)),j,(f /. i));
assume A1: ( i in dom f & j = i - 1 ) ; :: thesis: Ins ((Del (f,i)),j,(f /. i)) = f
then consider n being Nat such that
A2: ( len f = n + 1 & len (Del (f,i)) = n ) by FINSEQ_3:104;
dom f = Seg (n + 1) by A2, FINSEQ_1:def 3;
then consider ii being Nat such that
A3: ( i = ii & 1 <= ii & ii <= n + 1 ) by A1;
i - 1 < i - 0 by XREAL_1:15;
then j < n + 1 by A1, A3, XXREAL_0:2;
then A4: j <= n by NAT_1:13;
A5: len (Ins ((Del (f,i)),j,(f /. i))) = (len (Del (f,i))) + 1 by FINSEQ_5:69;

now :: thesis: for k being Nat st 1 <= k & k <= len (Ins ((Del (f,i)),j,(f /. i))) holds
(Ins ((Del (f,i)),j,(f /. i))) . k = f . k

let k be Nat; :: thesis: ( 1 <= k & k <= len (Ins ((Del (f,i)),j,(f /. i))) implies (Ins ((Del (f,i)),j,(f /. i))) . k = f . k )
assume A6: ( 1 <= k & k <= len (Ins ((Del (f,i)),j,(f /. i))) ) ; :: thesis: (Ins ((Del (f,i)),j,(f /. i))) . k = f . k

now :: thesis: (Ins ((Del (f,i)),j,(f /. i))) . k = f . k

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

suppose A8: k < i ; :: thesis: (Ins ((Del (f,i)),j,(f /. i))) . k = f . k

then k + 1 <= i by NAT_1:13;
then (k + 1) - 1 <= i - 1 by XREAL_1:9;
then ( 1 <= k & k <= len ((Del (f,i)) | j) ) by A6, A1, A4, A2, FINSEQ_1:59;
then k in Seg (len ((Del (f,i)) | j)) ;
then k in dom ((Del (f,i)) | j) by FINSEQ_1:def 3;
hence (Ins ((Del (f,i)),j,(f /. i))) . k = (Del (f,i)) . k by FINSEQ_5:72
.= f . k by A8, FINSEQ_3:110 ;
:: thesis: verum

end;

suppose A11: k = i ; :: thesis: (Ins ((Del (f,i)),j,(f /. i))) . k = f . k

S: f /. i = f . i by A1, PARTFUN1:def 6;
k = j + 1 by A1, A11;
then (Ins ((Del (f,i)),j,(f /. i))) . k = f . i by S, A2, A4, FINSEQ_5:73;
hence (Ins ((Del (f,i)),j,(f /. i))) . k = f . k by A11; :: thesis: verum

end;

suppose A13: k > i ; :: thesis: f . k = (Ins ((Del (f,i)),j,(f /. i))) . k

then reconsider k1 = k - 1 as Element of NAT by A3, INT_1:5, XXREAL_0:2;
A14: k - 1 <= (n + 1) - 1 by A6, A2, A5, XREAL_1:9;
i < k1 + 1 by A13;
then A16: j + 1 <= k - 1 by A1, NAT_1:13;
then (Ins ((Del (f,i)),j,(f /. i))) . (k1 + 1) = (Del (f,i)) . k1 by A14, A2, FINSEQ_5:74
.= f . (k1 + 1) by A16, A14, A2, A1, FINSEQ_3:111 ;
hence f . k = (Ins ((Del (f,i)),j,(f /. i))) . k ; :: thesis: verum

end;

end;

end;

hence (Ins ((Del (f,i)),j,(f /. i))) . k = f . k ; :: thesis: verum

end;

hence Ins ((Del (f,i)),j,(f /. i)) = f by A2, FINSEQ_5:69; :: thesis: verum