consider o being OperSymbol of S, p being Element of Args (o,(Free (S,X))) such that
A1: e = o -term p by Th17;
( e . {} = [o, the carrier of S] & main-constr e = (e . {}) `1 ) by A1, TREES_4:def 4, ABCMIZ_A:def 9;
hence main-constr e is OperSymbol of S ; :: thesis: verum