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