let T be TuringStr ; :: thesis: for s being All-State of T holds (Computation s) . 1 = Following s
let s be All-State of T; :: thesis: (Computation s) . 1 = Following s
(Computation s) . (0 + 1) = Following ((Computation s) . 0 ) by Def8
.= Following s by Def8 ;
hence (Computation s) . 1 = Following s ; :: thesis: verum