let z1, z2 be Tuple of n, BOOLEAN ; :: thesis: ( ( for i being Nat st i in Seg n holds
z1 /. i = ((x /. i) 'xor' ((Neg2 y) /. i)) 'xor' ((carry x,(Neg2 y)) /. i) ) & ( for i being Nat st i in Seg n holds
z2 /. i = ((x /. i) 'xor' ((Neg2 y) /. i)) 'xor' ((carry x,(Neg2 y)) /. i) ) implies z1 = z2 )
assume that
A6: for i being Nat st i in Seg n holds
z1 /. i = ((x /. i) 'xor' ((Neg2 y) /. i)) 'xor' ((carry x,(Neg2 y)) /. i) and
A7: for i being Nat st i in Seg n holds
z2 /. i = ((x /. i) 'xor' ((Neg2 y) /. i)) 'xor' ((carry x,(Neg2 y)) /. i) ; :: thesis: z1 = z2
A8: len z1 = n by FINSEQ_1:def 18;
A9: len z2 = n by FINSEQ_1:def 18;
A10: dom z1 = Seg n by A8, FINSEQ_1:def 3;

A11: now

let j be Nat; :: thesis: ( j in dom z1 implies z1 . j = z2 . j )
assume A12: j in dom z1 ; :: thesis: z1 . j = z2 . j
A13: Seg n = Seg (len z2) by FINSEQ_1:def 18;
A14: j in dom z2 by A10, A12, A13, FINSEQ_1:def 3;
thus z1 . j = z1 /. j by A12, PARTFUN1:def 8
.= ((x /. j) 'xor' ((Neg2 y) /. j)) 'xor' ((carry x,(Neg2 y)) /. j) by A6, A10, A12
.= z2 /. j by A7, A10, A12
.= z2 . j by A14, PARTFUN1:def 8 ; :: thesis: verum

end;

thus z1 = z2 by A8, A9, A11, FINSEQ_2:10; :: thesis: verum