let D be non empty set ; :: thesis: for s being FinSequence of D st s <> {} holds
ex w being FinSequence of D ex n being Element of D st s = <*n*> ^ w
let s be FinSequence of D; :: thesis: ( s <> {} implies ex w being FinSequence of D ex n being Element of D st s = <*n*> ^ w )
defpred S₁[ FinSequence of D] means ( $1 <> {} implies ex w being FinSequence of D ex n being Element of D st $1 = <*n*> ^ w );
A1: for s being FinSequence of D
for m being Element of D st S₁[s] holds
S₁[s ^ <*m*>]

proof

let s be FinSequence of D; :: thesis: for m being Element of D st S₁[s] holds
S₁[s ^ <*m*>]
let m be Element of D; :: thesis: ( S₁[s] implies S₁[s ^ <*m*>] )
assume A2: ( s <> {} implies ex w being FinSequence of D ex n being Element of D st s = <*n*> ^ w ) ; :: thesis: S₁[s ^ <*m*>]
assume s ^ <*m*> <> {} ; :: thesis: ex w being FinSequence of D ex n being Element of D st s ^ <*m*> = <*n*> ^ w

per cases ( s = {} or s <> {} ) ;

suppose A3: s = {} ; :: thesis: ex w being FinSequence of D ex n being Element of D st s ^ <*m*> = <*n*> ^ w

reconsider w = <*> D as FinSequence of D ;
take w ; :: thesis: ex n being Element of D st s ^ <*m*> = <*n*> ^ w
take n = m; :: thesis: s ^ <*m*> = <*n*> ^ w
thus s ^ <*m*> = <*m*> by A3, FINSEQ_1:34
.= <*n*> ^ w by FINSEQ_1:34 ; :: thesis: verum

end;

suppose s <> {} ; :: thesis: ex w being FinSequence of D ex n being Element of D st s ^ <*m*> = <*n*> ^ w

then consider w being FinSequence of D, n being Element of D such that
A4: s = <*n*> ^ w by A2;
take w ^ <*m*> ; :: thesis: ex n being Element of D st s ^ <*m*> = <*n*> ^ (w ^ <*m*>)
take n ; :: thesis: s ^ <*m*> = <*n*> ^ (w ^ <*m*>)
thus s ^ <*m*> = <*n*> ^ (w ^ <*m*>) by A4, FINSEQ_1:32; :: thesis: verum

end;

end;

end;

A5: S₁[ <*> D] ;
for p being FinSequence of D holds S₁[p] from FINSEQ_2:sch 2(A5, A1);
hence ( s <> {} implies ex w being FinSequence of D ex n being Element of D st s = <*n*> ^ w ) ; :: thesis: verum