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 c' being Element of M such that
A4: u = vect d,c' by Th55;
A5: a @ c' = b @ d by A1, A4, Th44
.= a @ c by A2, A3, Th44 ;
u + v = vect a,c by A1, A2, Th60
.= vect a,c' by A5, Th18
.= v + u by A3, A4, Th60 ;
hence u + v = v + u ; :: thesis: verum