:: deftheorem Def7 defines REL FREEALG:def 7 :
for f being non empty FinSequence of NAT
for X being set
for b₃ being Relation of ((dom f) \/ X),(((dom f) \/ X) *) holds
( b₃ = REL (f,X) iff for a being Element of (dom f) \/ X
for b being Element of ((dom f) \/ X) * holds
( [a,b] in b₃ iff ( a in dom f & f . a = len b ) ) );