let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A4: for p being FinSequence of F₁() st len p = i holds
P₁[p] ; :: thesis: S₁[i + 1]
let p be FinSequence of F₁(); :: thesis: ( len p = i + 1 implies P₁[p] )
assume A5: len p = i + 1 ; :: thesis: P₁[p]
then consider q being FinSequence of F₁(), x being Element of F₁() such that
A6: p = q ^ <*x*> by Th17;
len p = (len q) + 1 by A6, Th14;
hence P₁[p] by A2, A4, A5, A6; :: thesis: verum

let p be FinSequence of F₁(); :: thesis: ( len p = 0 implies P₁[p] )
assume len p = 0 ; :: thesis: P₁[p]
then p = <*> F₁() ;
hence P₁[p] by A1; :: thesis: verum