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

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