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 by NAT_1:14;
then A3: n in Seg n by FINSEQ_1:3;
n <= len F by FINSEQ_1:def 18;
then 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