let M be MidSp; :: thesis: for u, v being Vector of M holds u + v = v + u
let u, v be Vector of M; :: thesis: u + v = v + u
consider a being Element of M;
consider b being Element of M such that
A1: u = vect (a,b) by Th55;
consider c being Element of M such that
A2: v = vect (b,c) by Th55;
consider d being Element of M such that
A3: v = vect (a,d) by Th55;
consider c9 being Element of M such that
A4: u = vect (d,c9) by Th55;
A5: a @ c9 = b @ d by A1, A4, Th44
.= a @ c by A2, A3, Th44 ;
u + v = vect (a,c) by A1, A2, Th60
.= vect (a,c9) by A5, Th18
.= v + u by A3, A4, Th60 ;
hence u + v = v + u ; :: thesis: verum