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)
A2: v `2 <> 0. I by Th2;
w `2 <> 0. I by Th2;
then (v `2) * (w `2) <> 0. I by A2, VECTSP_2:def 5;
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 A2, VECTSP_2:def 5;
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))] by MCART_1:def 1
.= [((u `1) * ((v `1) * (w `1))),((u `2) * ((v `2) * (w `2)))] by MCART_1:def 2
.= [(((u `1) * (v `1)) * (w `1)),((u `2) * ((v `2) * (w `2)))] by GROUP_1:def 4
.= [(((u `1) * (v `1)) * (w `1)),(((u `2) * (v `2)) * (w `2))] by GROUP_1:def 4
.= [((s `1) * (w `1)),(((u `2) * (v `2)) * (w `2))] by MCART_1:def 1
.= pmult ((pmult (u,v)),w) by MCART_1:def 2 ;
hence pmult (u,(pmult (v,w))) = pmult ((pmult (u,v)),w) ; :: thesis: verum