let z1, z2 be Tuple of n,BOOLEAN ; :: thesis: ( ( for i being Nat st i in Seg n holds
z1 /. i = IFEQ i,1,TRUE ,FALSE ) & ( for i being Nat st i in Seg n holds
z2 /. i = IFEQ i,1,TRUE ,FALSE ) implies z1 = z2 )
assume that
A5: for i being Nat st i in Seg n holds
z1 /. i = IFEQ i,1,TRUE ,FALSE and
A6: for i being Nat st i in Seg n holds
z2 /. i = IFEQ i,1,TRUE ,FALSE ; :: thesis: z1 = z2
A7: ( len z1 = n & len z2 = n ) by FINSEQ_1:def 18;
then X: dom z1 = Seg n by FINSEQ_1:def 3;

now

let j be Nat; :: thesis: ( j in dom z1 implies z1 . j = z2 . j )
assume A8: j in dom z1 ; :: thesis: z1 . j = z2 . j
then A9: ( j in dom z1 & j in dom z2 ) by A7, X, FINSEQ_1:def 3;
thus z1 . j = z1 /. j by A8, PARTFUN1:def 8
.= IFEQ j,1,TRUE ,FALSE by A5, A8, X
.= z2 /. j by A6, A8, X
.= z2 . j by A9, PARTFUN1:def 8 ; :: thesis: verum

end;

hence z1 = z2 by A7, FINSEQ_2:10; :: thesis: verum