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;
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) ; :: thesis: verum