scheme :: MATGRP_0:sch 3
GLSubgroup{ F₁() -> Nat, F₂() -> Ring, P₁[ Matrix of F₂()] } :

ex H being strict Subgroup of GL (F₁(),F₂()) st
for X being invertible Matrix of F₁(),F₂() holds
( X in H iff P₁[X] )

provided

A1: for X, Y being invertible Matrix of F₁(),F₂() st P₁[X] & P₁[Y] holds
P₁[X * Y] and
A2: for X being invertible Matrix of F₁(),F₂() st P₁[X] holds
P₁[X ~ ] and
A3: P₁[ 1. (F₂(),F₁())]