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;
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 A5: i in dom p ; :: thesis: p . i = q . i
then A6: i in dom q by A2, A4, FINSEQ_1:def 3;
A7: p /. i = p . i by A5, PARTFUN1:def 6;
q /. i = q . i by A6, PARTFUN1:def 6;
hence p . i = q . i by A3, A4, A5, A7; :: thesis: verum

end;

hence p = q by A1, A2, FINSEQ_2:9; :: thesis: verum