let n be non empty 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:15
.= ((- 0 ) + (2 to_power n)) - 1 by A1, Th7
.= (2 to_power n) - 1 ; :: thesis: verum