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: ( u `2 <> 0. I & v `2 <> 0. I & w `2 <> 0. I ) by Th2;
then A2: (v `2 ) * (w `2 ) <> 0. I by VECTSP_2:def 5;
A3: (u `2 ) * (v `2 ) <> 0. I by A1, VECTSP_2:def 5;
reconsider t = [((v `1 ) * (w `1 )),((v `2 ) * (w `2 ))] as Element of Q. I by A2, Def1;
reconsider s = [((u `1 ) * (v `1 )),((u `2 ) * (v `2 ))] as Element of Q. I by A3, Def1;
A4: 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 ;
pmult u,v = [((u `1 ) * (v `1 )),((u `2 ) * (v `2 ))]
.= pmult v,u ;
hence ( pmult u,(pmult v,w) = pmult (pmult u,v),w & pmult u,v = pmult v,u ) by A4; :: thesis: verum