:: deftheorem defines value_at AOFA_A00:def 20 :
for B being non empty non void ManySortedSign
for X being non-empty ManySortedSet of the carrier of B
for T being non-empty b₂,b₁ -terms MSAlgebra over B
for C being image of T
for a being SortSymbol of B
for t being Element of T,a
for s being Function-yielding Function st ex h being ManySortedFunction of T,C ex Q being GeneratorSet of T st
( h is_homomorphism T,C & Q = doms s & s = h || Q ) holds
for b₈ being Element of C,a holds
( b₈ = t value_at (C,s) iff ex f being ManySortedFunction of T,C ex Q being GeneratorSet of T st
( f is_homomorphism T,C & Q = doms s & s = f || Q & b₈ = (f . a) . t ) );