for S, E being non void Signature st E is S -extension holds
for o being OperSymbol of S
for a being set
for r being Element of S
for r1 being Element of E st r = r1 & o is_of_type a,r holds
o is_of_type a,r1