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:1;
then A7: (k + 1) - 1 <= (len (SgmX (R,B))) - 1 by XREAL_1:9;
A8: (k + 1) - 1 = k + 0 ;
A9: len (SgmX (R,B)) = card B by A3, Th10
.= (card A) + 1 by A1, A2, CARD_2:41
.= (len (SgmX (R,A))) + 1 by A2, A3, Lm6, Th10 ;
then A10: dom (SgmX (R,B)) = Seg (len (Ins ((SgmX (R,A)),k,a))) by A6, FINSEQ_5:69
.= 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:1;
A15: i in dom (SgmX (R,B)) by FINSEQ_3:25, A12, A13;
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

then a = (SgmX (R,B)) . i by A5, PARTFUN1:def 6, A15;
hence (SgmX (R,B)) . i = (Ins ((SgmX (R,A)),k,a)) . (k + 1) by A9, A7, FINSEQ_5:73
.= (Ins ((SgmX (R,A)),k,a)) . i by A17 ;
:: thesis: verum

end;

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

now :: thesis: ( ( i < k + 1 & (SgmX (R,B)) . i = (Ins ((SgmX (R,A)),k,a)) . i ) or ( k + 1 <= i & (SgmX (R,B)) . i = (Ins ((SgmX (R,A)),k,a)) . i ) )

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:15;
then dom ((SgmX (R,A)) | (Seg k)) = Seg k by A9, A7, FINSEQ_1:17;
then SS: i in dom ((SgmX (R,A)) | (Seg k)) by A12, A19, FINSEQ_1:1;
then A20: i in dom ((SgmX (R,A)) | k) by FINSEQ_1:def 16;
A: i in dom (SgmX (R,A)) by RELAT_1:57, SS;
thus (SgmX (R,B)) . i = (SgmX (R,B)) /. i by A15, PARTFUN1:def 6
.= (SgmX (R,A)) /. i by A1, A2, A3, A4, A5, A8, A12, A14, A19, Th76
.= (SgmX (R,A)) . i by PARTFUN1:def 6, A
.= (Ins ((SgmX (R,A)),k,a)) . i by A20, FINSEQ_5:72 ; :: thesis: verum

end;

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

then a21: k + 1 < i by A18, XXREAL_0:1;
1 - 1 <= i - 1 by A12, XREAL_1:9;
then reconsider i9 = i - 1 as Element of NAT by INT_1:3;
A22: i9 + 1 = i + 0 ;
F: 1 <= k + 1 by FINSEQ_3:25, A4;
k + 1 < i9 + 1 by a21;
then 1 < i9 + 1 by F, XXREAL_0:2;
then 1 + 1 <= i9 + 1 by NAT_1:13;
then F1: 1 <= i9 by XREAL_1:6;
Z2: i9 + 1 in dom (Ins ((SgmX (R,A)),k,a)) by A16;
then i9 + 1 <= len (Ins ((SgmX (R,A)),k,a)) by FINSEQ_3:25;
then i9 + 1 <= (len (SgmX (R,A))) + 1 by FINSEQ_5:69;
then i9 <= len (SgmX (R,A)) by XREAL_1:6;
then F2: i9 in dom (SgmX (R,A)) by FINSEQ_3:25, F1;
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:9;
thus (SgmX (R,B)) . i = (SgmX (R,B)) /. (i9 + 1) by A15, PARTFUN1:def 6
.= (SgmX (R,A)) /. i9 by A1, A2, A3, A4, A5, A9, A24, A23, Th77
.= (SgmX (R,A)) . i9 by PARTFUN1:def 6, F2
.= (Ins ((SgmX (R,A)),k,a)) . (i9 + 1) by A9, A24, A23, FINSEQ_5:74
.= (Ins ((SgmX (R,A)),k,a)) /. (i9 + 1) by Z2, PARTFUN1:def 6
.= (Ins ((SgmX (R,A)),k,a)) . i by A16, PARTFUN1:def 6 ; :: 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:69;
hence SgmX (R,B) = Ins ((SgmX (R,A)),k,a) by A11, FINSEQ_1:14; :: thesis: verum