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