let C be initialized ConstructorSignature; :: thesis: for a being non positive expression of C, an_Adj C ex a' being expression of C, an_Adj C st
( a = (non_op C) term a' & Non a = a' )
let a be non positive expression of C, an_Adj C; :: thesis: ex a' being expression of C, an_Adj C st
( a = (non_op C) term a' & Non a = a' )
consider a' being expression of C, an_Adj C such that
A1: a = (non_op C) term a' by Def37;
A2: a = [non_op ,the carrier of C] -tree <*a'*> by A1, Th43;
take a' ; :: thesis: ( a = (non_op C) term a' & Non a = a' )
len <*a'*> = 1 by FINSEQ_1:57;
then a | <*0 *> = <*a'*> . (0 + 1) by A2, TREES_4:def 4
.= a' by FINSEQ_1:57 ;
hence ( a = (non_op C) term a' & Non a = a' ) by A1, Def36; :: thesis: verum