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 and
A2: a = (non_op C) term a' by Def38;
A3: a = [non_op ,the carrier of C] -tree <*a'*> by A2, Th43;
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' )
len <*a'*> = 1 by FINSEQ_1:57;
then a | <*0 *> = <*a'*> . (0 + 1) by A3, TREES_4:def 4
.= a' by FINSEQ_1:57 ;
hence ( a = (non_op C) term a' & Non a = a' ) by A2, Def36; :: thesis: verum