let X be set ; :: thesis: for f being FinSequence of X st f <> {} holds
ex g being FinSequence of X ex d being Element of X st f = g ^ <*d*>
let f be FinSequence of X; :: thesis: ( f <> {} implies ex g being FinSequence of X ex d being Element of X st f = g ^ <*d*> )
assume f <> {} ; :: thesis: ex g being FinSequence of X ex d being Element of X st f = g ^ <*d*>
then consider q being FinSequence, x being set such that
A1: f = q ^ <*x*> by FINSEQ_1:46;
reconsider q = q as FinSequence of X by A1, FINSEQ_1:36;
take q ; :: thesis: ex d being Element of X st f = q ^ <*d*>
take x ; :: thesis: ( x is Element of X & f = q ^ <*x*> )
<*x*> is FinSequence of X by A1, FINSEQ_1:36;
hence x is Element of X by Th3; :: thesis: f = q ^ <*x*>
thus f = q ^ <*x*> by A1; :: thesis: verum