let I be non empty non degenerated Abelian associative commutative domRing-like doubleLoopStr ; :: thesis: 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; :: thesis: 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;
X2: ( [((u `1) * (v `1)),((u `2) * (v `2))] `1 = (u `1) * (v `1) & [((u `1) * (v `1)),((u `2) * (v `2))] `2 = (u `2) * (v `2) ) ;
X1: ( [((v `1) * (w `1)),((v `2) * (w `2))] `1 = (v `1) * (w `1) & [((v `1) * (w `1)),((v `2) * (w `2))] `2 = (v `2) * (w `2) ) ;
pmult (u,(pmult (v,w))) = [((u `1) * ((v `1) * (w `1))),((u `2) * (t `2))] by X1
.= [((u `1) * ((v `1) * (w `1))),((u `2) * ((v `2) * (w `2)))] by X1
.= [(((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))] by X2
.= pmult ((pmult (u,v)),w) by X2 ;
hence pmult (u,(pmult (v,w))) = pmult ((pmult (u,v)),w) ; :: thesis: verum