set q = (S ^^ n) -tail p;
S ^^ ((n + 1) + m) = (S ^^ (n + 1)) ^ (S ^^ m) by Th10
.= ((S ^^ n) ^ (S ^^ 1)) ^ (S ^^ m) by Th10
.= (S ^^ n) ^ (S ^ (S ^^ m)) by Th2 ;
then (S ^^ n) -tail p in S ^ (S ^^ m) by Th54;
hence S -head ((S ^^ n) -tail p) is Element of S by Th54; :: thesis: verum