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 A4: ( k + 1 in dom (SgmX R,B) & (SgmX R,B) /. (k + 1) = a ) ; :: thesis: SgmX R,B = Ins (SgmX R,A),k,a
A5: (k + 1) - 1 = k + 0 ;
set sgb = SgmX R,B;
set sga = Ins (SgmX R,A),k,a;
A6: len (SgmX R,B) = card B by A3, TRIANG_1:9
.= (card A) + 1 by A1, A2, CARD_2:54
.= (len (SgmX R,A)) + 1 by A2, A3, Lm4, TRIANG_1:9 ;
then A7: len (SgmX R,B) = len (Ins (SgmX R,A),k,a) by FINSEQ_5:72;
A8: dom (SgmX R,B) = Seg (len (SgmX R,B)) by FINSEQ_1:def 3;
then A9: 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 ;
k + 1 <= len (SgmX R,B) by A4, A8, FINSEQ_1:3;
then A10: (k + 1) - 1 <= (len (SgmX R,B)) - 1 by XREAL_1:11;
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 A11: ( 1 <= i & i <= len (SgmX R,B) ) ; :: thesis: (SgmX R,B) . i = (Ins (SgmX R,A),k,a) . i
then A12: i in Seg (len (SgmX R,B)) by FINSEQ_1:3;
then A13: i in dom (SgmX R,B) by FINSEQ_1:def 3;
A14: i in dom (Ins (SgmX R,A),k,a) by A9, A12, FINSEQ_1:def 3;

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

suppose A15: 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 A13, PARTFUN1:def 8
.= (Ins (SgmX R,A),k,a) /. (k + 1) by A4, A6, A10, A15, FINSEQ_5:76
.= (Ins (SgmX R,A),k,a) . i by A14, A15, PARTFUN1:def 8 ; :: thesis: verum

end;

suppose A16: 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 A17: 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 A6, A10, FINSEQ_1:21;
then i in dom ((SgmX R,A) | (Seg k)) by A11, A17, FINSEQ_1:3;
then A18: i in dom ((SgmX R,A) | k) by FINSEQ_1:def 15;
thus (SgmX R,B) . i = (SgmX R,B) /. i by A13, PARTFUN1:def 8
.= (SgmX R,A) /. i by A1, A2, A3, A4, A5, A11, A12, A17, Th11
.= (Ins (SgmX R,A),k,a) /. i by A18, FINSEQ_5:75
.= (Ins (SgmX R,A),k,a) . i by A14, PARTFUN1:def 8 ; :: thesis: verum

end;

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

then A19: k + 1 < i by A16, XXREAL_0:1;
1 - 1 <= i - 1 by A11, XREAL_1:11;
then reconsider i' = i - 1 as Element of NAT by INT_1:16;
A20: i' + 1 = i + 0 ;
A21: i' <= (len (SgmX R,B)) - 1 by A11, XREAL_1:11;
A22: k + 1 <= i' by A19, A20, NAT_1:13;
thus (SgmX R,B) . i = (SgmX R,B) /. (i' + 1) by A13, PARTFUN1:def 8
.= (SgmX R,A) /. i' by A1, A2, A3, A4, A6, A21, A22, Th12
.= (Ins (SgmX R,A),k,a) /. (i' + 1) by A6, A21, A22, FINSEQ_5:77
.= (Ins (SgmX R,A),k,a) . i by A14, 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;

hence SgmX R,B = Ins (SgmX R,A),k,a by A7, FINSEQ_1:18; :: thesis: verum