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 u' being Vector of M such that
A2: u + u' = ID M by Th65;
v = v + (ID M) by Th64
.= (u + u') + v by A2, Th66
.= (u' + u) + v by Th66
.= u' + (u + w) by A1, Th63
.= (u' + u) + w by Th63
.= (ID M) + w by A2, Th66
.= w + (ID M) by Th66 ;
hence v = w by Th64; :: thesis: verum