let n be non empty 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 & n <= len F ) by FINSEQ_1:def 18, NAT_1:14;
then A3: n in Seg n by FINSEQ_1:3;
F /. n = F . n by A2, FINSEQ_4:24
.= FALSE by A1, A3, FUNCOP_1:13 ;
then Intval F = Absval F by BINARI_2:def 3;
hence Intval F = 0 by A1, BINARI_3:7; :: thesis: verum