theorem Th45: :: ABCMIZ_1:45

for C being initialized ConstructorSignature
for o being OperSymbol of C st len (the_arity_of o) = 2 holds
for a, b being expression of C st ex s1, s2 being SortSymbol of C st
( s1 = (the_arity_of o) . 1 & s2 = (the_arity_of o) . 2 & a is expression of C,s1 & b is expression of C,s2 ) holds
[o, the carrier of C] -tree <*a,b*> is expression of C, the_result_sort_of o