let C be initialized ConstructorSignature; :: thesis: for a being negative expression of C, an_Adj C ex a' being positive expression of C, an_Adj C st
( a = (non_op C) term a' & Non a = a' )
let a be negative expression of C, an_Adj C; :: thesis: ex a' being positive 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' is positive & a = (non_op C) term a' ) by NEGATIVE;
A2: a = [non_op ,the carrier of C] -tree <*a'*> by A1, ThNon;
reconsider a' = a' as positive expression of C, an_Adj C by A1;
take a' ; :: thesis: ( a = (non_op C) term a' & Non a = a' )
( 0 < 1 & 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, NON'OPA; :: thesis: verum