let C be initialized ConstructorSignature; :: thesis: for a, b being expression of C, an_Adj C
for t being expression of C, a_Type C holds (non_op C) term a <> (ast C) term b,t
let a, b be expression of C, an_Adj C; :: thesis: for t being expression of C, a_Type C holds (non_op C) term a <> (ast C) term b,t
let t be expression of C, a_Type C; :: thesis: (non_op C) term a <> (ast C) term b,t
assume (non_op C) term a = (ast C) term b,t ; :: thesis: contradiction
then (non_op C) term a = [* ,the carrier of C] -tree <*b,t*> by ThAst;
then ((non_op C) term a) . {} = [* ,the carrier of C] by TREES_4:def 4;
then ([non_op ,the carrier of C] -tree <*a*>) . {} = [* ,the carrier of C] by ThNon;
then [non_op ,the carrier of C] = [* ,the carrier of C] by TREES_4:def 4;
hence contradiction by ZFMISC_1:33; :: thesis: verum