let n be non zero Nat; :: thesis: for z1, z2 being Tuple of n,BOOLEAN
for d1, d2 being Element of BOOLEAN holds add_ovfl z1,z2 = (carry (z1 ^ <*d1*>),(z2 ^ <*d2*>)) /. (n + 1)
let z1, z2 be Tuple of n,BOOLEAN ; :: thesis: for d1, d2 being Element of BOOLEAN holds add_ovfl z1,z2 = (carry (z1 ^ <*d1*>),(z2 ^ <*d2*>)) /. (n + 1)
let d1, d2 be Element of BOOLEAN ; :: thesis: add_ovfl z1,z2 = (carry (z1 ^ <*d1*>),(z2 ^ <*d2*>)) /. (n + 1)
A1: n in Seg n by FINSEQ_1:5;
then A2: (carry (z1 ^ <*d1*>),(z2 ^ <*d2*>)) /. n = (carry z1,z2) /. n by Th43;
A3: z1 /. n = (z1 ^ <*d1*>) /. n by A1, Th2;
A4: z2 /. n = (z2 ^ <*d2*>) /. n by A1, Th2;
( 1 <= n & n < n + 1 ) by NAT_1:14, XREAL_1:31;
hence add_ovfl z1,z2 = (carry (z1 ^ <*d1*>),(z2 ^ <*d2*>)) /. (n + 1) by A2, A3, A4, Def5; :: thesis: verum