let AFV be WeakAffVect; :: thesis: for o being Element of AFV
for a, b, c being Element of (GroupVect (AFV,o)) holds (a + b) + c = a + (b + c)
let o be Element of AFV; :: thesis: for a, b, c being Element of (GroupVect (AFV,o)) holds (a + b) + c = a + (b + c)
let a, b, c be Element of (GroupVect (AFV,o)); :: thesis: (a + b) + c = a + (b + c)
reconsider a9 = a, b9 = b, c9 = c as Element of AFV ;
set p = b + c;
set q = a + b;
reconsider p9 = b + c, q9 = a + b as Element of AFV ;
reconsider x9 = a + (b + c), y9 = (a + b) + c as Element of AFV ;
consider x99 being Element of AFV such that
A1: x9,p9 // c9,x99 by Def1;
x9 = Padd (o,a9,p9) by Def6;
then o,a9 // p9,x9 by Def5;
then A2: a9,o // x9,p9 by Th7;
c9,x99 // x9,p9 by A1, Th3;
then A3: a9,o // c9,x99 by A2, Def1;
q9 = Padd (o,a9,b9) by Def6;
then o,a9 // b9,q9 by Def5;
then o,b9 // a9,q9 by Def1;
then A4: a9,q9 // o,b9 by Th3;
p9 = Padd (o,b9,c9) by Def6;
then o,b9 // c9,p9 by Def5;
then c9,p9 // o,b9 by Th3;
then a9,q9 // c9,p9 by A4, Def1;
then A5: q9,o // p9,x99 by A3, Def1;
x9,c9 // p9,x99 by A1, Def1;
then q9,o // x9,c9 by A5, Def1;
then o,q9 // c9,x9 by Th7;
then A6: c9,x9 // o,q9 by Th3;
y9 = Padd (o,q9,c9) by Def6;
then o,q9 // c9,y9 by Def5;
then c9,y9 // o,q9 by Th3;
then c9,y9 // c9,x9 by A6, Def1;
hence (a + b) + c = a + (b + c) by Th4; :: thesis: verum