let n be non zero Nat; :: thesis: for F being Tuple of n, BOOLEAN st F = 0* n holds
Intval F = 0
let F be Tuple of n, BOOLEAN ; :: thesis: ( F = 0* n implies Intval F = 0 )
assume A1: F = 0* n ; :: thesis: Intval F = 0
A2: 1 <= n by NAT_1:14;
n <= len F by CARD_1:def 7;
then F /. n = F . n by A2, FINSEQ_4:15
.= FALSE by A1 ;
then Intval F = Absval F by BINARI_2:def 3;
hence Intval F = 0 by A1, BINARI_3:6; :: thesis: verum