let C be initialized ConstructorSignature; :: thesis: for a being expression of C, an_Adj C
for f being valuation of C holds (Non a) at f = Non (a at f)
let a be expression of C, an_Adj C; :: thesis: for f being valuation of C holds (Non a) at f = Non (a at f)
let f be valuation of C; :: thesis: (Non a) at f = Non (a at f)

per cases ( a is positive or not a is positive ) ;

suppose a is positive ; :: thesis: (Non a) at f = Non (a at f)

then reconsider b = a as positive expression of C, an_Adj C ;
reconsider af = b at f as positive expression of C, an_Adj C ;
thus (Non a) at f = ((non_op C) term b) at f by Th44
.= (non_op C) term af by SUBST
.= Non (a at f) by Th44 ; :: thesis: verum

end;

suppose not a is positive ; :: thesis: (Non a) at f = Non (a at f)

then consider b being expression of C, an_Adj C such that
A0: ( a = (non_op C) term b & Non a = b ) by Th45g;
A1: a at f = (non_op C) term (b at f) by A0, SUBST;
then not a at f is positive by POSITIVE;
then ex k being expression of C, an_Adj C st
( a at f = (non_op C) term k & Non (a at f) = k ) by Th45g;
hence (Non a) at f = Non (a at f) by A0, A1, ThNon'; :: thesis: verum

end;

end;