let q, p be PartState of S; :: thesis: ( q = p +* (Start-At (0,S)) implies q = q +* (Start-At (0,S)) )
assume A1: q = p +* (Start-At (0,S)) ; :: thesis: q = q +* (Start-At (0,S))
hence q = (p +* (Start-At (0,S))) +* (Start-At (0,S))
.= q +* (Start-At (0,S)) by A1 ;
:: thesis: verum