let n be non zero Nat; :: thesis: for F being Tuple of n, BOOLEAN st F = 0* n holds
Absval ('not' F) = (2 to_power n) - 1
let F be Tuple of n, BOOLEAN ; :: thesis: ( F = 0* n implies Absval ('not' F) = (2 to_power n) - 1 )
assume A1: F = 0* n ; :: thesis: Absval ('not' F) = (2 to_power n) - 1
thus Absval ('not' F) = ((- (Absval F)) + (2 to_power n)) - 1 by BINARI_2:13
.= ((- 0) + (2 to_power n)) - 1 by A1, Th6
.= (2 to_power n) - 1 ; :: thesis: verum