let AFV be WeakAffVect; 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; 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)); (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; verum