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
proof
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;
hence Sgm (I \/ {x}) = (Sgm I) ^ (Sgm {x}) by A1, A5, FINSEQ_3:42
.= (Sgm I) ^ <*x*> by FINSEQ_3:44, A2 ;
:: thesis: verum