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 a' = a, b' = b, c' = c as Element of AFV ;
set p = b + c;
set q = a + b;
reconsider p' = b + c, q' = a + b as Element of AFV ;
reconsider x' = a + (b + c), y' = (a + b) + c as Element of AFV ;
p' = Padd o,b',c' by Def7;
then A1: o,b' // c',p' by Def5;
q' = Padd o,a',b' by Def7;
then o,a' // b',q' by Def5;
then o,b' // a',q' by Def1;
then A2: a',q' // o,b' by Th4;
c',p' // o,b' by A1, Th4;
then A3: a',q' // c',p' by A2, Def1;
consider x'' being Element of AFV such that
A4: x',p' // c',x'' by Def1;
A5: c',x'' // x',p' by A4, Th4;
x' = Padd o,a',p' by Def7;
then o,a' // p',x' by Def5;
then a',o // x',p' by Th8;
then a',o // c',x'' by A5, Def1;
then A6: q',o // p',x'' by A3, Def1;
x',c' // p',x'' by A4, Def1;
then q',o // x',c' by A6, Def1;
then o,q' // c',x' by Th8;
then A7: c',x' // o,q' by Th4;
y' = Padd o,q',c' by Def7;
then o,q' // c',y' by Def5;
then c',y' // o,q' by Th4;
then c',y' // c',x' by A7, Def1;
hence (a + b) + c = a + (b + c) by Th5; :: thesis: verum