theorem :: MSAFREE4:53

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for o being OperSymbol of S
for a1, a2 being FinSequence st a1 in Args (o,(TermAlg S)) & a2 in Args (o,(TermAlg S)) & ( for i being Nat st i in dom (the_arity_of o) holds
for s being SortSymbol of S st s = (the_arity_of o) . i holds
for t1, t2 being Element of (TermAlg S),s st t1 = a1 . i & t2 = a2 . i holds
A |= t1 '=' t2 ) holds
for t1, t2 being Element of (TermAlg S),(the_result_sort_of o) st t1 = [o, the carrier of S] -tree a1 & t2 = [o, the carrier of S] -tree a2 holds
A |= t1 '=' t2