:: deftheorem defines -supported AOFA_A00:def 25 :
for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of the carrier of S
for T being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself VarMSAlgebra over S
for C being image of T
for G being GeneratorSystem over S,X,T holds
( G is C -supported iff ( FreeGen X is ManySortedSubset of the generators of G & ( for s being SortSymbol of S holds
( dom ( the supported-term of G . s) = G . s & ( for t being Element of G,s holds
( ( the supported-term of G . s) . t is ManySortedFunction of vf t, the Sorts of T & ( t in (FreeGen X) . s implies ( supp-term t = id (s -singleton t) & supp-var t = t ) ) & ( for v being Element of C -States the generators of G st (v . s) . (supp-var t) = (v . s) . t holds
for r being SortSymbol of S
for x being Element of (FreeGen X) . r
for q being Element of the Sorts of T . r st x in (vf t) . r & q = ((supp-term t) . r) . x holds
(v . r) . x = q value_at (C,v) ) & ( t nin (FreeGen X) . s implies for H being ManySortedSubset of the generators of G st H = FreeGen X holds
for v being Element of C,s
for f being ManySortedFunction of the generators of G, the Sorts of C st f in C -States the generators of G holds
for u being ManySortedFunction of FreeGen X, the Sorts of C st ( for a being SortSymbol of S
for z being Element of (FreeGen X) . a st z in (vf t) . a holds
for q being Element of T,a st q = ((supp-term t) . a) . z holds
(u . a) . z = q value_at (C,((f || H) +* (s,(supp-var t),v))) ) holds
for H being ManySortedSubset of the Sorts of T st H = FreeGen X holds
for h being ManySortedFunction of T,C st h is_homomorphism T,C & h || H = u holds
v = (h . s) . t ) ) ) ) ) ) );