for p1, p2 being FinSequence of K st len p1 = n & ( for i, j being Nat st i in dom p1 & j = p . i holds
p1 . i = M * (i,j) ) & len p2 = n & ( for i, j being Nat st i in dom p2 & j = p . i holds
p2 . i = M * (i,j) ) holds
p1 = p2
proof
let p1,
p2 be
FinSequence of
K;
( len p1 = n & ( for i, j being Nat st i in dom p1 & j = p . i holds
p1 . i = M * (i,j) ) & len p2 = n & ( for i, j being Nat st i in dom p2 & j = p . i holds
p2 . i = M * (i,j) ) implies p1 = p2 )
assume that A4:
len p1 = n
and A5:
for
i,
j being
Nat st
i in dom p1 &
j = p . i holds
p1 . i = M * (
i,
j)
and A6:
len p2 = n
and A7:
for
i,
j being
Nat st
i in dom p2 &
j = p . i holds
p2 . i = M * (
i,
j)
;
p1 = p2
A8:
dom p2 = Seg n
by A6, FINSEQ_1:def 3;
A9:
dom p1 = Seg n
by A4, FINSEQ_1:def 3;
for
i being
Nat st
i in Seg n holds
p1 . i = p2 . i
hence
p1 = p2
by A9, A8, FINSEQ_1:13;
verum
end;
hence
for b1, b2 being FinSequence of K st len b1 = n & ( for i, j being Nat st i in dom b1 & j = p . i holds
b1 . i = M * (i,j) ) & len b2 = n & ( for i, j being Nat st i in dom b2 & j = p . i holds
b2 . i = M * (i,j) ) holds
b1 = b2
; verum