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
set a = the Element of M;
consider b being Element of M such that
A1: u = vect ( the Element of M,b) by Th35;
consider c being Element of M such that
A2: v = vect (b,c) by Th35;
consider d being Element of M such that
A3: v = vect ( the Element of M,d) by Th35;
consider c9 being Element of M such that
A4: u = vect (d,c9) by Th35;
A5: the Element of M @ c9 = b @ d by A1, A4, Th29
.= the Element of M @ c by A2, A3, Th29 ;
u + v = vect ( the Element of M,c) by A1, A2, Th40
.= vect ( the Element of M,c9) by A5, Th8
.= v + u by A3, A4, Th40 ;
hence u + v = v + u ; :: thesis: verum