theorem :: AOFA_000:37

for A being free Universal_Algebra
for o1, o2 being Element of Operations A
for p1, p2 being FinSequence st p1 in dom o1 & p2 in dom o2 & o1 . p1 = o2 . p2 holds
( o1 = o2 & p1 = p2 )