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