theorem Th11: :: ABCMIZ_A:11

for C being initialized standardized ConstructorSignature
for e being expression of C holds
( ex x being Element of Vars st
( e = x -term C & e . {} = [x,a_Term] ) or ex o being OperSymbol of C st
( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) )