let x be object ; :: thesis: for q being FinSubsequence st Seq q = <*x*> holds
ex i being Element of NAT st q = {[i,x]}
let q be FinSubsequence; :: thesis: ( Seq q = <*x*> implies ex i being Element of NAT st q = {[i,x]} )
assume Seq q = <*x*> ; :: thesis: ex i being Element of NAT st q = {[i,x]}
then A1: Seq q = {[1,x]} by FINSEQ_1:def 5;
then A2: dom (Seq q) = {1} by RELAT_1:9;
A3: rng (Seq q) = {x} by A1, RELAT_1:9;
A4: Seq q = q * (Sgm (dom q)) by FINSEQ_1:def 15;
A5: rng (Sgm (dom q)) = dom q by FINSEQ_1:50;
then A6: {1} = dom (Sgm (dom q)) by A2, A4, RELAT_1:27;
A7: rng (Seq q) = rng q by A4, A5, RELAT_1:28;
consider n being Nat such that
A8: dom q c= Seg n by FINSEQ_1:def 12;
Seg (card (dom q)) = {1} by A6, Th38;
then card (dom q) = card {1} by FINSEQ_1:57;
then consider y being object such that
A9: dom q = {y} by CARD_1:29;
y in dom q by A9, TARSKI:def 1;
then y in Seg n by A8;
then reconsider y = y as Element of NAT ;
q = {[y,x]} by A3, A7, A9, RELAT_1:189;
hence ex i being Element of NAT st q = {[i,x]} ; :: thesis: verum