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 object 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*>
<*x*> is FinSequence of X by A1, FINSEQ_1:36;
then reconsider x = x as Element of X by Th3;
take x ; :: thesis: f = q ^ <*x*>
thus f = q ^ <*x*> by A1; :: thesis: verum