per cases ( p is S -headed or not p is S -headed ) ;

suppose p is S -headed ; :: thesis: ex b₁ being FinSequence st p = (S -head p) ^ b₁

hence ex b₁ being FinSequence st p = (S -head p) ^ b₁ by Def22; :: thesis: verum

end;

suppose not p is S -headed ; :: thesis: ex b₁ being FinSequence st p = (S -head p) ^ b₁

then S -head p = {} by Def22;
then p = (S -head p) ^ p by FINSEQ_1:34;
hence ex b₁ being FinSequence st p = (S -head p) ^ b₁ ; :: thesis: verum

end;

end;