for p being FinSequence st p in GRZ-ops holds
dom p = Seg 1 by Lm2;
hence GRZ-ops is Polish-language by POLNOT_1:45; :: thesis: verum