let X be non empty set ; :: thesis: for A being finite Subset of X
for a being Element of X st not a in A holds
for B being finite Subset of X st B = {a} \/ A holds
for R being Order of X st R linearly_orders B holds
for k being Element of NAT st k + 1 in dom (SgmX R,B) & (SgmX R,B) /. (k + 1) = a holds
SgmX R,B = Ins (SgmX R,A),k,a
let A be finite Subset of X; :: thesis: for a being Element of X st not a in A holds
for B being finite Subset of X st B = {a} \/ A holds
for R being Order of X st R linearly_orders B holds
for k being Element of NAT st k + 1 in dom (SgmX R,B) & (SgmX R,B) /. (k + 1) = a holds
SgmX R,B = Ins (SgmX R,A),k,a
let a be Element of X; :: thesis: ( not a in A implies for B being finite Subset of X st B = {a} \/ A holds
for R being Order of X st R linearly_orders B holds
for k being Element of NAT st k + 1 in dom (SgmX R,B) & (SgmX R,B) /. (k + 1) = a holds
SgmX R,B = Ins (SgmX R,A),k,a )
assume A1: not a in A ; :: thesis: for B being finite Subset of X st B = {a} \/ A holds
for R being Order of X st R linearly_orders B holds
for k being Element of NAT st k + 1 in dom (SgmX R,B) & (SgmX R,B) /. (k + 1) = a holds
SgmX R,B = Ins (SgmX R,A),k,a
let B be finite Subset of X; :: thesis: ( B = {a} \/ A implies for R being Order of X st R linearly_orders B holds
for k being Element of NAT st k + 1 in dom (SgmX R,B) & (SgmX R,B) /. (k + 1) = a holds
SgmX R,B = Ins (SgmX R,A),k,a )
assume A2: B = {a} \/ A ; :: thesis: for R being Order of X st R linearly_orders B holds
for k being Element of NAT st k + 1 in dom (SgmX R,B) & (SgmX R,B) /. (k + 1) = a holds
SgmX R,B = Ins (SgmX R,A),k,a
let R be Order of X; :: thesis: ( R linearly_orders B implies for k being Element of NAT st k + 1 in dom (SgmX R,B) & (SgmX R,B) /. (k + 1) = a holds
SgmX R,B = Ins (SgmX R,A),k,a )
assume A3: R linearly_orders B ; :: thesis: for k being Element of NAT st k + 1 in dom (SgmX R,B) & (SgmX R,B) /. (k + 1) = a holds
SgmX R,B = Ins (SgmX R,A),k,a
let k be Element of NAT ; :: thesis: ( k + 1 in dom (SgmX R,B) & (SgmX R,B) /. (k + 1) = a implies SgmX R,B = Ins (SgmX R,A),k,a )
assume that
A4: k + 1 in dom (SgmX R,B) and
A5: (SgmX R,B) /. (k + 1) = a ; :: thesis: SgmX R,B = Ins (SgmX R,A),k,a
set sgb = SgmX R,B;
set sga = Ins (SgmX R,A),k,a;
A6: dom (SgmX R,B) = Seg (len (SgmX R,B)) by FINSEQ_1:def 3;
then k + 1 <= len (SgmX R,B) by A4, FINSEQ_1:3;
then A7: (k + 1) - 1 <= (len (SgmX R,B)) - 1 by XREAL_1:11;
A8: (k + 1) - 1 = k + 0 ;
A9: len (SgmX R,B) = card B by A3, PRE_POLY:11
.= (card A) + 1 by A1, A2, CARD_2:54
.= (len (SgmX R,A)) + 1 by A2, A3, Lm4, PRE_POLY:11 ;
then A10: dom (SgmX R,B) = Seg (len (Ins (SgmX R,A),k,a)) by A6, FINSEQ_5:72
.= dom (Ins (SgmX R,A),k,a) by FINSEQ_1:def 3 ;
A11: for i being Nat st 1 <= i & i <= len (SgmX R,B) holds
(SgmX R,B) . i = (Ins (SgmX R,A),k,a) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len (SgmX R,B) implies (SgmX R,B) . i = (Ins (SgmX R,A),k,a) . i )
assume that
A12: 1 <= i and
A13: i <= len (SgmX R,B) ; :: thesis: (SgmX R,B) . i = (Ins (SgmX R,A),k,a) . i
A14: i in Seg (len (SgmX R,B)) by A12, A13, FINSEQ_1:3;
then A15: i in dom (SgmX R,B) by FINSEQ_1:def 3;
A16: i in dom (Ins (SgmX R,A),k,a) by A10, A14, FINSEQ_1:def 3;

per cases ( i = k + 1 or i <> k + 1 ) ;

suppose A17: i = k + 1 ; :: thesis: (SgmX R,B) . i = (Ins (SgmX R,A),k,a) . i

thus (SgmX R,B) . i = (SgmX R,B) /. i by A15, PARTFUN1:def 8
.= (Ins (SgmX R,A),k,a) /. (k + 1) by A5, A9, A7, A17, FINSEQ_5:76
.= (Ins (SgmX R,A),k,a) . i by A16, A17, PARTFUN1:def 8 ; :: thesis: verum

end;

suppose A18: i <> k + 1 ; :: thesis: (SgmX R,B) . i = (Ins (SgmX R,A),k,a) . i

now

per cases ( i < k + 1 or k + 1 <= i ) ;

case i < k + 1 ; :: thesis: (SgmX R,B) . i = (Ins (SgmX R,A),k,a) . i

then A19: i <= k by NAT_1:13;
(SgmX R,A) | (Seg k) is FinSequence by FINSEQ_1:19;
then dom ((SgmX R,A) | (Seg k)) = Seg k by A9, A7, FINSEQ_1:21;
then i in dom ((SgmX R,A) | (Seg k)) by A12, A19, FINSEQ_1:3;
then A20: i in dom ((SgmX R,A) | k) by FINSEQ_1:def 15;
thus (SgmX R,B) . i = (SgmX R,B) /. i by A15, PARTFUN1:def 8
.= (SgmX R,A) /. i by A1, A2, A3, A4, A5, A8, A12, A14, A19, Th11
.= (Ins (SgmX R,A),k,a) /. i by A20, FINSEQ_5:75
.= (Ins (SgmX R,A),k,a) . i by A16, PARTFUN1:def 8 ; :: thesis: verum

end;

case A21: k + 1 <= i ; :: thesis: (SgmX R,B) . i = (Ins (SgmX R,A),k,a) . i

1 - 1 <= i - 1 by A12, XREAL_1:11;
then reconsider i9 = i - 1 as Element of NAT by INT_1:16;
A22: i9 + 1 = i + 0 ;
k + 1 < i by A18, A21, XXREAL_0:1;
then A23: k + 1 <= i9 by A22, NAT_1:13;
A24: i9 <= (len (SgmX R,B)) - 1 by A13, XREAL_1:11;
thus (SgmX R,B) . i = (SgmX R,B) /. (i9 + 1) by A15, PARTFUN1:def 8
.= (SgmX R,A) /. i9 by A1, A2, A3, A4, A5, A9, A24, A23, Th12
.= (Ins (SgmX R,A),k,a) /. (i9 + 1) by A9, A24, A23, FINSEQ_5:77
.= (Ins (SgmX R,A),k,a) . i by A16, PARTFUN1:def 8 ; :: thesis: verum

end;

end;

end;

hence (SgmX R,B) . i = (Ins (SgmX R,A),k,a) . i ; :: thesis: verum

end;

end;

end;

len (SgmX R,B) = len (Ins (SgmX R,A),k,a) by A9, FINSEQ_5:72;
hence SgmX R,B = Ins (SgmX R,A),k,a by A11, FINSEQ_1:18; :: thesis: verum