let n be Nat; :: thesis: for p, q being Tuple of n, BOOLEAN st len p = n & len q = n & ( for i being Nat st i in Seg n holds
p /. i = q /. i ) holds
p = q
let p, q be Tuple of n, BOOLEAN ; :: thesis: ( len p = n & len q = n & ( for i being Nat st i in Seg n holds
p /. i = q /. i ) implies p = q )
assume that
A1: len p = n and
A2: len q = n and
A3: for i being Nat st i in Seg n holds
p /. i = q /. i ; :: thesis: p = q
A4: dom p = Seg n by A1, FINSEQ_1:def 3;
A5: for i being Nat st i in dom p holds
p . i = q . i

proof

let i be Nat; :: thesis: ( i in dom p implies p . i = q . i )
assume A6: i in dom p ; :: thesis: p . i = q . i
A7: i in dom q by A2, A4, A6, FINSEQ_1:def 3;
A8: p /. i = p . i by A6, PARTFUN1:def 8;
A9: q /. i = q . i by A7, PARTFUN1:def 8;
thus p . i = q . i by A3, A4, A6, A8, A9; :: thesis: verum

end;

thus p = q by A1, A2, A5, FINSEQ_2:10; :: thesis: verum