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

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

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

hence p . m = q . m by A4; :: thesis: verum