g . n is Element of (bool (bool PM)) * ;
hence g . n is FinSequence of bool (bool PM) ; :: thesis: verum