let M be MidSp; :: thesis: for u, v, w being Vector of M holds (u + v) + w = u + (v + w)

let u, v, w be Vector of M; :: thesis: (u + v) + w = u + (v + w)

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: w = vect (c,d) by Th35;

(u + v) + w = (vect ( the Element of M,c)) + w by A1, A2, Th40

.= vect ( the Element of M,d) by A3, Th40

.= (vect ( the Element of M,b)) + (vect (b,d)) by Th40

.= u + (v + w) by A1, A2, A3, Th40 ;

hence (u + v) + w = u + (v + w) ; :: thesis: verum

let u, v, w be Vector of M; :: thesis: (u + v) + w = u + (v + w)

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: w = vect (c,d) by Th35;

(u + v) + w = (vect ( the Element of M,c)) + w by A1, A2, Th40

.= vect ( the Element of M,d) by A3, Th40

.= (vect ( the Element of M,b)) + (vect (b,d)) by Th40

.= u + (v + w) by A1, A2, A3, Th40 ;

hence (u + v) + w = u + (v + w) ; :: thesis: verum