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 & pmult u,v = pmult v,u )
let u, v, w be Element of Q. I; :: thesis: ( pmult u,(pmult v,w) = pmult (pmult u,v),w & pmult u,v = pmult v,u )
A1: pmult u,v = [((u `1 ) * (v `1 )),((u `2 ) * (v `2 ))]
.= pmult v,u ;
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 & pmult u,v = pmult v,u ) by A1; :: thesis: verum