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