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