defpred S₁[ FinSequence of NAT ] means ( $1 <> {} implies ex w being FinSequence of NAT ex n being Nat st $1 = <*n*> ^ w );
A1: for s being FinSequence of NAT
for m being Element of NAT st S₁[s] holds
S₁[s ^ <*m*>]

proof

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

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

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

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

end;

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

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

end;

end;

end;

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