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

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

hence
x = y
by Th14; :: thesis: verum
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;W . (a,(p . m)) = x . m by A3;

hence x . m = y . m by A4; :: thesis: verum