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
A3: ( len p1 = n & ( for i being Nat st i in Seg n holds
p1 . i = M * i,i ) ) and
A4: ( len p2 = n & ( for i being Nat st i in Seg n holds
p2 . i = M * i,i ) ) ; :: thesis: p1 = p2
A5: ( dom p1 = Seg n & dom p2 = Seg n ) by A3, A4, FINSEQ_1:def 3;

now

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

end;

hence p1 = p2 by A5, FINSEQ_1:17; :: thesis: verum