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

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