let x be set ; :: 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:23;
A3: rng (Seq q) = {x} by A1, RELAT_1:23;
A4: Seq q = q * (Sgm (dom q)) by FINSEQ_1:def 14;
rng (Sgm (dom q)) = dom q by FINSEQ_1:71;
then A5: ( {1} = dom (Sgm (dom q)) & rng (Seq q) = rng q ) by A2, A4, RELAT_1:46, RELAT_1:47;
consider n being Nat such that
A6: dom q c= Seg n by FINSEQ_1:def 12;
Seg (card (dom q)) = {1} by A5, A6, FINSEQ_3:45;
then card (dom q) = card {1} by FINSEQ_1:78;
then consider y being set such that
A7: dom q = {y} by CARD_1:49;
y in dom q by A7, TARSKI:def 1;
then y in Seg n by A6;
then reconsider y = y as Element of NAT ;
q = {[y,x]} by A3, A5, A7, PRE_CIRC:2;
hence ex i being Element of NAT st q = {[i,x]} ; :: thesis: verum