let I be non empty non degenerated Abelian add-associative associative commutative distributive domRing-like doubleLoopStr ; for u, v, w being Element of Q. I holds padd (u,(padd (v,w))) = padd ((padd (u,v)),w)
let u, v, w be Element of Q. I; padd (u,(padd (v,w))) = padd ((padd (u,v)),w)
A1: ((u `1) * ((v `2) * (w `2))) + ((((v `1) * (w `2)) + ((w `1) * (v `2))) * (u `2)) =
((u `1) * ((v `2) * (w `2))) + ((((v `1) * (w `2)) * (u `2)) + (((w `1) * (v `2)) * (u `2)))
by VECTSP_1:def 3
.=
(((u `1) * ((v `2) * (w `2))) + (((v `1) * (w `2)) * (u `2))) + (((w `1) * (v `2)) * (u `2))
by RLVECT_1:def 3
.=
(((u `1) * ((v `2) * (w `2))) + (((v `1) * (w `2)) * (u `2))) + ((w `1) * ((v `2) * (u `2)))
by GROUP_1:def 3
.=
((((u `1) * (v `2)) * (w `2)) + (((v `1) * (w `2)) * (u `2))) + ((w `1) * ((v `2) * (u `2)))
by GROUP_1:def 3
.=
((((u `1) * (v `2)) * (w `2)) + (((v `1) * (u `2)) * (w `2))) + ((w `1) * ((v `2) * (u `2)))
by GROUP_1:def 3
.=
((((u `1) * (v `2)) + ((v `1) * (u `2))) * (w `2)) + ((w `1) * ((v `2) * (u `2)))
by VECTSP_1:def 3
;
A2:
v `2 <> 0. I
by Th2;
u `2 <> 0. I
by Th2;
then
(u `2) * (v `2) <> 0. I
by A2, VECTSP_2:def 1;
then reconsider s = [(((u `1) * (v `2)) + ((v `1) * (u `2))),((u `2) * (v `2))] as Element of Q. I by Def1;
w `2 <> 0. I
by Th2;
then
(v `2) * (w `2) <> 0. I
by A2, VECTSP_2:def 1;
then reconsider t = [(((v `1) * (w `2)) + ((w `1) * (v `2))),((v `2) * (w `2))] as Element of Q. I by Def1;
padd (u,(padd (v,w))) =
[(((u `1) * (t `2)) + ((((v `1) * (w `2)) + ((w `1) * (v `2))) * (u `2))),((u `2) * (t `2))]
.=
[(((u `1) * ((v `2) * (w `2))) + ((((v `1) * (w `2)) + ((w `1) * (v `2))) * (u `2))),((u `2) * (t `2))]
.=
[(((u `1) * ((v `2) * (w `2))) + ((((v `1) * (w `2)) + ((w `1) * (v `2))) * (u `2))),((u `2) * ((v `2) * (w `2)))]
.=
[(((u `1) * ((v `2) * (w `2))) + ((((v `1) * (w `2)) + ((w `1) * (v `2))) * (u `2))),(((u `2) * (v `2)) * (w `2))]
by GROUP_1:def 3
;
then padd (u,(padd (v,w))) =
[(((s `1) * (w `2)) + ((w `1) * ((v `2) * (u `2)))),(((u `2) * (v `2)) * (w `2))]
by A1
.=
[(((s `1) * (w `2)) + ((w `1) * (s `2))),(((u `2) * (v `2)) * (w `2))]
.=
padd ((padd (u,v)),w)
;
hence
padd (u,(padd (v,w))) = padd ((padd (u,v)),w)
; verum