let i, k, x be Nat; :: thesis: for I being set st I c= Seg k & k < x & x in Seg i holds

Sgm (I \/ {x}) = (Sgm I) ^ <*x*>

let I be set ; :: thesis: ( I c= Seg k & k < x & x in Seg i implies Sgm (I \/ {x}) = (Sgm I) ^ <*x*> )

assume that

A1: I c= Seg k and

A2: k < x and

A3: x in Seg i ; :: thesis: Sgm (I \/ {x}) = (Sgm I) ^ <*x*>

A5: {x} c= Seg i by A3, ZFMISC_1:31;

for m, n being Nat st m in I & n in {x} holds

m < n

.= (Sgm I) ^ <*x*> by FINSEQ_3:44, A2 ;

:: thesis: verum

Sgm (I \/ {x}) = (Sgm I) ^ <*x*>

let I be set ; :: thesis: ( I c= Seg k & k < x & x in Seg i implies Sgm (I \/ {x}) = (Sgm I) ^ <*x*> )

assume that

A1: I c= Seg k and

A2: k < x and

A3: x in Seg i ; :: thesis: Sgm (I \/ {x}) = (Sgm I) ^ <*x*>

A5: {x} c= Seg i by A3, ZFMISC_1:31;

for m, n being Nat st m in I & n in {x} holds

m < n

proof

hence Sgm (I \/ {x}) =
(Sgm I) ^ (Sgm {x})
by A1, A5, FINSEQ_3:42
let m, n be Nat; :: thesis: ( m in I & n in {x} implies m < n )

assume A6: ( m in I & n in {x} ) ; :: thesis: m < n

then A8: n = x by TARSKI:def 1;

( 1 <= m & m <= k ) by A1, A6, FINSEQ_1:1;

hence m < n by A8, A2, XXREAL_0:2; :: thesis: verum

end;assume A6: ( m in I & n in {x} ) ; :: thesis: m < n

then A8: n = x by TARSKI:def 1;

( 1 <= m & m <= k ) by A1, A6, FINSEQ_1:1;

hence m < n by A8, A2, XXREAL_0:2; :: thesis: verum

.= (Sgm I) ^ <*x*> by FINSEQ_3:44, A2 ;

:: thesis: verum