:: BINARI_2 semantic presentation

begin

        Lm1:  for n being Nat
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
proof
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;
end;