let A be set ; :: thesis: for p being FinSequence of A st len p <> 0 holds
ex q being FinSequence of A ex d being Element of A st p = q ^ <*d*>
let p be FinSequence of A; :: thesis: ( len p <> 0 implies ex q being FinSequence of A ex d being Element of A st p = q ^ <*d*> )
assume A1: len p <> 0 ; :: thesis: ex q being FinSequence of A ex d being Element of A st p = q ^ <*d*>
then p <> {} ;
then consider q being FinSequence, d being object such that
A2: p = q ^ <*d*> by FINSEQ_1:46;
for i being Nat st i in dom q holds
q . i in A
proof
let i be Nat; :: thesis: ( i in dom q implies q . i in A )
assume i in dom q ; :: thesis: q . i in A
then ( p . i = q . i & i in dom p ) by A2, Th13, FINSEQ_1:def 7;
hence q . i in A by Th9; :: thesis: verum
end;
then A3: q is FinSequence of A by Th10;
len p in Seg (len p) by A1, FINSEQ_1:3;
then A4: len p in dom p by FINSEQ_1:def 3;
len p = (len q) + 1 by A2, Th14;
then p . (len p) = d by A2, FINSEQ_1:42;
then d is Element of A by A4, Th9;
hence ex q being FinSequence of A ex d being Element of A st p = q ^ <*d*> by A2, A3; :: thesis: verum