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