let z1 be Tuple of 2, BOOLEAN ; :: thesis: ( z1 = <*TRUE *> ^ <*FALSE *> implies Intval z1 = 1 )
assume A1: z1 = <*TRUE *> ^ <*FALSE *> ; :: thesis: Intval z1 = 1
consider k1, k2 being Element of NAT such that
A2: Binary z1 = <*k1,k2*> by FINSEQ_2:120;
A3: z1 = <*TRUE ,FALSE *> by A1, FINSEQ_1:def 9;
A4: z1 /. 1 = TRUE by A3, FINSEQ_4:26;
A5: z1 /. 2 = FALSE by A3, FINSEQ_4:26;
A6: ( 1 in Seg 1 & Seg 1 c= Seg 2 ) by FINSEQ_1:5, FINSEQ_1:7;
A7: (Binary z1) /. 1 = IFEQ (z1 /. 1),FALSE ,0 ,(2 to_power (1 -' 1)) by A6, BINARITH:def 6
.= 2 to_power (1 -' 1) by A4, FUNCOP_1:def 8 ;
A8: 1 - 1 = 0 ;
A9: 1 -' 1 = 0 by A8, XREAL_0:def 2;
A10: (Binary z1) /. 1 = 1 by A7, A9, POWER:29;
A11: 2 in Seg 2 by FINSEQ_1:5;
A12: (Binary z1) /. 2 = IFEQ (z1 /. 2),FALSE ,0 ,(2 to_power (2 -' 1)) by A11, BINARITH:def 6
.= 0 by A5, FUNCOP_1:def 8 ;
A13: ( (Binary z1) /. 1 = k1 & (Binary z1) /. 2 = k2 ) by A2, FINSEQ_4:26;
A14: Absval z1 = addnat $$ <*1,0 *> by A2, A10, A12, A13, BINARITH:def 7
.= addnat $$ (<*1*> ^ <*0 *>) by FINSEQ_1:def 9
.= addnat . (addnat $$ <*1*>),(addnat $$ <*0 *>) by FINSOP_1:6
.= addnat . 1,(addnat $$ <*0 *>) by FINSOP_1:12
.= addnat . 1,0 by FINSOP_1:12
.= 1 + 0 by BINOP_2:def 23
.= 1 ;
thus Intval z1 = 1 by A5, A14, Def3; :: thesis: verum