reconsider b = a as Element of GRZ-formula-set ;
<*a*> = <*b*> ;
hence <*a*> is FinSequence of GRZ-formula-set ; :: thesis: verum