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