FG b is not equivalent to EFG b, since the former is a path formula and the latter is a state formula. Above, the context makes the two exchangeable. The E quantifier comes from the outer A quantifier and is generated by the following rule (page 42):

A[ψ B φ] = A[ψ B (Eφ)]