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

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

hence
s1 = s2
by A5, FUNCT_1:2; :: thesis: verum
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;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