let p1, p2 be sequence of L; :: thesis: ( ( for n being Element of NAT holds p1 . n = (p . n) / (p . ((len p) -' 1)) ) & ( for n being Element of NAT holds p2 . n = (p . n) / (p . ((len p) -' 1)) ) implies p1 = p2 )
assume that
A2: for n being Element of NAT holds p1 . n = (p . n) / (p . ((len p) -' 1)) and
A3: for n being Element of NAT holds p2 . n = (p . n) / (p . ((len p) -' 1)) ; :: thesis: p1 = p2

now :: thesis: for n being Element of NAT holds p1 . n = p2 . n

let n be Element of NAT ; :: thesis: p1 . n = p2 . n
thus p1 . n = (p . n) / (p . ((len p) -' 1)) by A2
.= p2 . n by A3 ; :: thesis: verum

end;

hence p1 = p2 by FUNCT_2:63; :: thesis: verum