:: deftheorem defines signature UNIALG_1:def 4 :
for U1 being non empty partial non-empty UAStr
for b₂ being FinSequence of NAT holds
( b₂ = signature U1 iff ( len b₂ = len the charact of U1 & ( for n being Nat st n in dom b₂ holds
for h being non empty homogeneous PartFunc of ( the carrier of U1 *), the carrier of U1 st h = the charact of U1 . n holds
b₂ . n = arity h ) ) );