let M be MidSp; :: thesis: for u, v, w being Vector of M st u + v = u + w holds
v = w
let u, v, w be Vector of M; :: thesis: ( u + v = u + w implies v = w )
assume A1: u + v = u + w ; :: thesis: v = w
consider u9 being Vector of M such that
A2: u + u9 = ID M by Th45;
v = v + (ID M) by Th44
.= (u + u9) + v by A2, Th46
.= (u9 + u) + v by Th46
.= u9 + (u + w) by A1, Th43
.= (u9 + u) + w by Th43
.= (ID M) + w by A2, Th46
.= w + (ID M) by Th46 ;
hence v = w by Th44; :: thesis: verum