let I be non empty non degenerated Abelian add-associative associative commutative distributive domRing-like doubleLoopStr ; for u, v, w being Element of Q. I holds
( padd u,(padd v,w) = padd (padd u,v),w & padd u,v = padd v,u )
let u, v, w be Element of Q. I; ( padd u,(padd v,w) = padd (padd u,v),w & padd u,v = padd v,u )
A1: ((u `1 ) * ((v `2 ) * (w `2 ))) + ((((v `1 ) * (w `2 )) + ((w `1 ) * (v `2 ))) * (u `2 )) =
((u `1 ) * ((v `2 ) * (w `2 ))) + ((((v `1 ) * (w `2 )) * (u `2 )) + (((w `1 ) * (v `2 )) * (u `2 )))
by VECTSP_1:def 12
.=
(((u `1 ) * ((v `2 ) * (w `2 ))) + (((v `1 ) * (w `2 )) * (u `2 ))) + (((w `1 ) * (v `2 )) * (u `2 ))
by RLVECT_1:def 6
.=
(((u `1 ) * ((v `2 ) * (w `2 ))) + (((v `1 ) * (w `2 )) * (u `2 ))) + ((w `1 ) * ((v `2 ) * (u `2 )))
by GROUP_1:def 4
.=
((((u `1 ) * (v `2 )) * (w `2 )) + (((v `1 ) * (w `2 )) * (u `2 ))) + ((w `1 ) * ((v `2 ) * (u `2 )))
by GROUP_1:def 4
.=
((((u `1 ) * (v `2 )) * (w `2 )) + (((v `1 ) * (u `2 )) * (w `2 ))) + ((w `1 ) * ((v `2 ) * (u `2 )))
by GROUP_1:def 4
.=
((((u `1 ) * (v `2 )) + ((v `1 ) * (u `2 ))) * (w `2 )) + ((w `1 ) * ((v `2 ) * (u `2 )))
by VECTSP_1:def 12
;
A2:
v `2 <> 0. I
by Th2;
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 `2 )) + ((v `1 ) * (u `2 ))),((u `2 ) * (v `2 ))] as Element of Q. I by Def1;
A3: padd u,v =
[(((u `1 ) * (v `2 )) + ((v `1 ) * (u `2 ))),((u `2 ) * (v `2 ))]
.=
padd v,u
;
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 `2 )) + ((w `1 ) * (v `2 ))),((v `2 ) * (w `2 ))] as Element of Q. I by Def1;
padd u,(padd v,w) =
[(((u `1 ) * (t `2 )) + ((((v `1 ) * (w `2 )) + ((w `1 ) * (v `2 ))) * (u `2 ))),((u `2 ) * (t `2 ))]
by MCART_1:def 1
.=
[(((u `1 ) * ((v `2 ) * (w `2 ))) + ((((v `1 ) * (w `2 )) + ((w `1 ) * (v `2 ))) * (u `2 ))),((u `2 ) * (t `2 ))]
by MCART_1:def 2
.=
[(((u `1 ) * ((v `2 ) * (w `2 ))) + ((((v `1 ) * (w `2 )) + ((w `1 ) * (v `2 ))) * (u `2 ))),((u `2 ) * ((v `2 ) * (w `2 )))]
by MCART_1:def 2
.=
[(((u `1 ) * ((v `2 ) * (w `2 ))) + ((((v `1 ) * (w `2 )) + ((w `1 ) * (v `2 ))) * (u `2 ))),(((u `2 ) * (v `2 )) * (w `2 ))]
by GROUP_1:def 4
;
then padd u,(padd v,w) =
[(((s `1 ) * (w `2 )) + ((w `1 ) * ((v `2 ) * (u `2 )))),(((u `2 ) * (v `2 )) * (w `2 ))]
by A1, MCART_1:def 1
.=
[(((s `1 ) * (w `2 )) + ((w `1 ) * (s `2 ))),(((u `2 ) * (v `2 )) * (w `2 ))]
by MCART_1:def 2
.=
padd (padd u,v),w
by MCART_1:def 2
;
hence
( padd u,(padd v,w) = padd (padd u,v),w & padd u,v = padd v,u )
by A3; verum