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 Th46;
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 Th43;
then [non_op, the carrier of C] = [*, the carrier of C] by TREES_4:def 4;
hence contradiction by XTUPLE_0:1; :: thesis: verum