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 S1[ 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 S1[s] holds
S1[s ^ <*m*>]
proof
let s be FinSequence of D; :: thesis: for m being Element of D st S1[s] holds
S1[s ^ <*m*>]
let m be Element of D; :: thesis: ( S1[s] implies S1[s ^ <*m*>] )
assume A2: ( s <> {} implies ex w being FinSequence of D ex n being Element of D st s = <*n*> ^ w ) ; :: thesis: S1[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: S1[ <*> D] ;
for p being FinSequence of D holds S1[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