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

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