let M be MidSp; :: thesis: for x, a, x9 being Element of M st x @ a = x9 @ a holds
x = x9
let x, a, 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 Def4;
x = x @ (y @ a) by A2, Def4
.= (x @ y) @ (x9 @ a) by A1, Th16
.= x @ (x @ x9) by A2, Def4 ;
then x = x @ x9 by Th17;
hence x = x9 by Th17; :: thesis: verum