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