let C be initialized ConstructorSignature; :: thesis: for e being expression of C holds
( e is compound iff for x being Element of Vars holds not e = x -term C )
let e be expression of C; :: thesis: ( e is compound iff for x being Element of Vars holds not e = x -term C )
( ex x being variable st e = x -term C or ex c being constructor OperSymbol of C ex p being FinSequence of QuasiTerms C st
( len p = len (the_arity_of c) & e = c -trm p ) or ex a being expression of C, an_Adj C st e = (non_op C) term a or ex a being expression of C, an_Adj C ex t being expression of C, a_Type C st e = (ast C) term (a,t) ) by ABCMIZ_1:53;
hence ( e is compound iff for x being Element of Vars holds not e = x -term C ) ; :: thesis: verum