let p1, p2 be FinSequence of K; :: thesis: ( len p1 = n & ( for i being Nat st i in Seg n holds
p1 . i = M * (i,i) ) & len p2 = n & ( for i being Nat st i in Seg n holds
p2 . i = M * (i,i) ) implies p1 = p2 )
assume that
A2: len p1 = n and
A3: for i being Nat st i in Seg n holds
p1 . i = M * (i,i) and
A4: len p2 = n and
A5: for i being Nat st i in Seg n holds
p2 . i = M * (i,i) ; :: thesis: p1 = p2

A6: now :: thesis: for i being Nat st i in Seg n holds
p1 . i = p2 . i

let i be Nat; :: thesis: ( i in Seg n implies p1 . i = p2 . i )
assume A7: i in Seg n ; :: thesis: p1 . i = p2 . i
then p1 . i = M * (i,i) by A3;
hence p1 . i = p2 . i by A5, A7; :: thesis: verum

end;

( dom p1 = Seg n & dom p2 = Seg n ) by A2, A4, FINSEQ_1:def 3;
hence p1 = p2 by A6, FINSEQ_1:13; :: thesis: verum