let n be non zero Nat; :: thesis: for z being Tuple of n, BOOLEAN st z = 0* n holds
('not' z) + (Bin1 n) = z
let z be Tuple of n, BOOLEAN ; :: thesis: ( z = 0* n implies ('not' z) + (Bin1 n) = z )
assume A1: z = 0* n ; :: thesis: ('not' z) + (Bin1 n) = z
then A2: add_ovfl (('not' z),(Bin1 n)) = TRUE by Th23;
Absval (('not' z) + (Bin1 n)) = ((Absval (('not' z) + (Bin1 n))) + (2 to_power n)) - (2 to_power n)
.= ((Absval (('not' z) + (Bin1 n))) + (IFEQ ((add_ovfl (('not' z),(Bin1 n))),FALSE,0,(2 to_power n)))) - (2 to_power n) by A2, FUNCOP_1:def 8
.= ((Absval ('not' z)) + (Absval (Bin1 n))) - (2 to_power n) by BINARITH:21
.= ((((- (Absval z)) + (2 to_power n)) - 1) + (Absval (Bin1 n))) - (2 to_power n) by BINARI_2:13
.= ((((- (Absval z)) + (2 to_power n)) - 1) + 1) - (2 to_power n) by Th11
.= - 0 by A1, Th6
.= Absval z by A1, Th6 ;
hence ('not' z) + (Bin1 n) = z by Th2; :: thesis: verum