let M be MidSp; :: thesis: for a, x, x9 being Element of M st x @ a = x9 @ a holds
x = x9
let a, x, x9 be Element of M; :: thesis: ( x @ a = x9 @ a implies x = x9 )
assume A1: x @ a = x9 @ a ; :: thesis: x = x9
consider y being Element of M such that
A2: y @ a = x by Def3;
x = x @ (y @ a) by A2, Def3
.= (x @ y) @ (x9 @ a) by A1, Th6
.= x @ (x @ x9) by A2, Def3 ;
then x = x @ x9 by Th7;
hence x = x9 by Th7; :: thesis: verum