let p be FinSequence; :: thesis: for x being object
for k being Nat st k in dom p & k < x .. p holds
p . k <> x
let x be object ; :: 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;
( p " {x} c= dom p & dom p = Seg (len p) ) by FINSEQ_1:def 3, RELAT_1:132;
then a1: p " {x} is included_in_Seg ;
then rng (Sgm (p " {x})) = p " {x} by FINSEQ_1:def 14;
then k in rng (Sgm (p " {x})) by A1, A3, A4, FUNCT_1:def 7;
then consider y being object such that
A6: y in dom (Sgm (p " {x})) and
A7: (Sgm (p " {x})) . y = k by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A6;

A8: now :: thesis: 1 < y

assume not 1 < y ; :: thesis: contradiction
then ( 1 = y or y < 1 ) by XXREAL_0:1;
hence contradiction by A2, A6, A7, FINSEQ_3:24, 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:1;
hence contradiction by a1, A2, A7, A8, FINSEQ_1:def 14; :: thesis: verum