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 Th59
.= (non_op C) term af by Def60
.= Non (a at f) by Th59 ; :: 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
A1: a = (non_op C) term b and
A2: Non a = b by Th60;
A3: a at f = (non_op C) term (b at f) by A1, Def60;
then not a at f is 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 Th60;
hence (Non a) at f = Non (a at f) by A2, A3, Th44; :: thesis: verum

end;

end;