let C be initialized ConstructorSignature; :: thesis: for a, b being expression of C, an_Adj C st (non_op C) term a = (non_op C) term b holds
a = b
let a, b be expression of C, an_Adj C; :: thesis: ( (non_op C) term a = (non_op C) term b implies a = b )
assume (non_op C) term a = (non_op C) term b ; :: thesis: a = b
then [non_op, the carrier of C] -tree <*a*> = (non_op C) term b by Th43
.= [non_op, the carrier of C] -tree <*b*> by Th43 ;
then <*a*> = <*b*> by TREES_4:15;
hence a = b by FINSEQ_1:76; :: thesis: verum