let z1 be Tuple of 2, BOOLEAN ; :: thesis: ( z1 = <*FALSE*> ^ <*FALSE*> implies Intval z1 = 0 )
assume A1: z1 = <*FALSE*> ^ <*FALSE*> ; :: thesis: Intval z1 = 0
consider k1, k2 being Element of NAT such that
A2: Binary z1 = <*k1,k2*> by FINSEQ_2:100;
A3: z1 = <*FALSE,FALSE*> by A1, FINSEQ_1:def 9;
then A4: z1 /. 1 = FALSE by FINSEQ_4:17;
A5: z1 /. 2 = FALSE by A3, FINSEQ_4:17;
( 1 in Seg 1 & Seg 1 c= Seg 2 ) by FINSEQ_1:3, FINSEQ_1:5;
then A6: (Binary z1) /. 1 = IFEQ ((z1 /. 1),FALSE,0,(2 to_power (1 -' 1))) by BINARITH:def 3
.= 0 by A4, FUNCOP_1:def 8 ;
2 in Seg 2 by FINSEQ_1:3;
then A7: (Binary z1) /. 2 = IFEQ ((z1 /. 2),FALSE,0,(2 to_power (2 -' 1))) by BINARITH:def 3
.= 0 by A5, FUNCOP_1:def 8 ;
( (Binary z1) /. 1 = k1 & (Binary z1) /. 2 = k2 ) by A2, FINSEQ_4:17;
then Absval z1 = addnat $$ <*0,0*> by A2, A6, A7, BINARITH:def 4
.= addnat $$ (<*0*> ^ <*0*>) by FINSEQ_1:def 9
.= addnat . ((addnat $$ <*0*>),(addnat $$ <*0*>)) by FINSOP_1:5
.= addnat . (0,(addnat $$ <*0*>)) by FINSOP_1:11
.= addnat . (0,0) by FINSOP_1:11
.= 0 + 0 by BINOP_2:def 23
.= 0 ;
hence Intval z1 = 0 by A5, Def3; :: thesis: verum