theorem :: POLYDIFF:31

for n being Nat
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for x, y being Element of L holds (seq (n,x)) - (seq (n,y)) = seq (n,(x - y))