let x, y be Tuple of (n + 1),W; :: thesis: ( ( 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) ; :: thesis: x = y
for m being Nat of n holds x . m = y . m

proof

let m be Nat of n; :: thesis: x . m = y . m
W . a,(p . m) = x . m by A3;
hence x . m = y . m by A4; :: thesis: verum

end;

hence x = y by Th16; :: thesis: verum