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