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: x in {x} by TARSKI:def 1;
A5: ( 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} by FINSEQ_1:def 13;
then k in rng (Sgm (p " {x})) by A1, A3, A4, FUNCT_1:def 13;
then consider y being set such that
A6: y in dom (Sgm (p " {x})) and
A7: (Sgm (p " {x})) . y = k by FUNCT_1:def 5;
reconsider y = y as Element of NAT by A6;

A8: now

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

end;

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