let C be initialized ConstructorSignature; :: thesis: for a being non positive expression of C, an_Adj C ex a9 being expression of C, an_Adj C st
( a = (non_op C) term a9 & Non a = a9 )
let a be non positive expression of C, an_Adj C; :: thesis: ex a9 being 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: a = (non_op C) term a9 by Def37;
A2: a = [non_op, the carrier of C] -tree <*a9*> by A1, Th43;
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 A2, TREES_4:def 4
.= a9 by FINSEQ_1:40 ;
hence ( a = (non_op C) term a9 & Non a = a9 ) by A1, Def36; :: thesis: verum