for n being Nat
for e being object holds (Segm (n + 1)) --> e = ((Segm n) --> e) ^ <%e%>