let x, y be Tuple of (n + 1),W; ( ( for m being Nat of n holds x . m = W . (a,(p . m)) ) & ( for m being Nat of n holds y . m = W . (a,(p . m)) ) implies x = y )
assume that
A3:
for m being Nat of n holds x . m = W . (a,(p . m))
and
A4:
for m being Nat of n holds y . m = W . (a,(p . m))
; x = y
for m being Nat of n holds x . m = y . m
hence
x = y
by Th14; verum