set Y = the non-empty basic GeneratorSet of T;
set SV = the ManySortedFunction of the non-empty basic GeneratorSet of T, FreeGen X;
set ST = the ManySortedMSSet of the non-empty basic GeneratorSet of T, the carrier of S;
take G = GeneratorSystem(# the non-empty basic GeneratorSet of T, the ManySortedFunction of the non-empty basic GeneratorSet of T, FreeGen X, the ManySortedMSSet of the non-empty basic GeneratorSet of T, the carrier of S #); :: thesis: G is basic
thus the generators of G is basic ; :: according to AOFA_A01:def 5 :: thesis: verum