let f be 1 -element natural-valued positive FinSequence; :: thesis: ex a being positive Nat st f = <*a*>
f is FinSequence of NAT by FINSEQ_1:103;
then consider a being Element of NAT such that
A1: f = <*a*> by FINSEQ_2:97;
reconsider a = a as positive Nat by A1;
take a ; :: thesis: f = <*a*>
thus f = <*a*> by A1; :: thesis: verum