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