let s1, s2 be sequence of L; :: thesis: ( ( for i being Nat holds s1 . i = p . (m * i) ) & ( for i being Nat holds s2 . i = p . (m * i) ) implies s1 = s2 )
assume that
A3: for i being Nat holds s1 . i = p . (m * i) and
A4: for i being Nat holds s2 . i = p . (m * i) ; :: thesis: s1 = s2
A5: ( dom s1 = NAT & NAT = dom s2 ) by FUNCT_2:def 1;
for x being object st x in dom s1 holds
s1 . x = s2 . x

proof

let x be object ; :: thesis: ( x in dom s1 implies s1 . x = s2 . x )
assume x in dom s1 ; :: thesis: s1 . x = s2 . x
then reconsider i = x as Element of NAT ;
thus s1 . x = p . (m * i) by A3
.= s2 . x by A4 ; :: thesis: verum

end;

hence s1 = s2 by A5, FUNCT_1:2; :: thesis: verum