:: deftheorem defines struct-invariant MSAFREE5:def 32 :
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of the carrier of S
for T being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds
( T is struct-invariant iff for o being OperSymbol of S
for p being Element of Args (o,T) st (Den (o,T)) . p = (Den (o,(Free (S,X)))) . p holds
for s being SortSymbol of S
for x1, x2 being Element of X . s holds (Den (o,T)) . ((Hom (T,x1,x2)) # p) = (Den (o,(Free (S,X)))) . ((Hom (T,x1,x2)) # p) );