set Y = the V3() basic GeneratorSet of T;
set SV = the ManySortedFunction of the V3() basic GeneratorSet of T, FreeGen X;
set ST = the ManySortedMSSet of the V3() basic GeneratorSet of T, the carrier of S;
take G = GeneratorSystem(# the V3() basic GeneratorSet of T, the ManySortedFunction of the V3() basic GeneratorSet of T, FreeGen X, the ManySortedMSSet of the V3() 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