let C be initialized ConstructorSignature; 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; 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; (non_op C) term a <> (ast C) term (b,t)
assume
(non_op C) term a = (ast C) term (b,t)
; 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; verum