let p be FinSequence; :: thesis: for x being set
for k being Nat st k in dom p & k < x .. p holds
p . k <> x
let x be set ; :: thesis: for k being Nat st k in dom p & k < x .. p holds
p . k <> x
let k be Nat; :: thesis: ( k in dom p & k < x .. p implies p . k <> x )
set q = Sgm (p " {x});
assume that
A1: k in dom p and
A2: k < x .. p and
A3: p . k = x ; :: thesis: contradiction
A4: ( p " {x} c= dom p & dom p = Seg (len p) ) by FINSEQ_1:def 3, RELAT_1:167;
then ( rng (Sgm (p " {x})) = p " {x} & x in {x} ) by FINSEQ_1:def 13, TARSKI:def 1;
then k in rng (Sgm (p " {x})) by A1, A3, FUNCT_1:def 13;
then consider y being set such that
A5: y in dom (Sgm (p " {x})) and
A6: (Sgm (p " {x})) . y = k by FUNCT_1:def 5;
A7: dom (Sgm (p " {x})) = Seg (len (Sgm (p " {x}))) by FINSEQ_1:def 3;
reconsider y = y as Element of NAT by A5;

now

assume not 1 < y ; :: thesis: contradiction
then ( 1 = y or y < 1 ) by XXREAL_0:1;
hence contradiction by A2, A5, A6, FINSEQ_3:26, NAT_1:14; :: thesis: verum

end;

then ( 1 <= 1 & 1 < y & y <= len (Sgm (p " {x})) ) by A5, A7, FINSEQ_1:3;
hence contradiction by A2, A4, A6, FINSEQ_1:def 13; :: thesis: verum