let R be commutative Ring; :: thesis: for S being non empty multiplicatively-closed Subset of R
for x, y, z being Element of Frac S holds Fracadd (x,(Fracadd (y,z))) = Fracadd ((Fracadd (x,y)),z)
let S be non empty multiplicatively-closed Subset of R; :: thesis: for x, y, z being Element of Frac S holds Fracadd (x,(Fracadd (y,z))) = Fracadd ((Fracadd (x,y)),z)
let x, y, z be Element of Frac S; :: thesis: Fracadd (x,(Fracadd (y,z))) = Fracadd ((Fracadd (x,y)),z)
Fracadd ((Fracadd (x,y)),z) = [(((((x `1) * (y `2)) * (z `2)) + (((y `1) * (x `2)) * (z `2))) + ((z `1) * ((x `2) * (y `2)))),(((x `2) * (y `2)) * (z `2))] by VECTSP_1:def 7
.= [((((x `1) * ((y `2) * (z `2))) + (((y `1) * (x `2)) * (z `2))) + ((z `1) * ((x `2) * (y `2)))),(((x `2) * (y `2)) * (z `2))] by GROUP_1:def 3
.= [((((x `1) * ((y `2) * (z `2))) + (((y `1) * (z `2)) * (x `2))) + ((z `1) * ((y `2) * (x `2)))),(((x `2) * (y `2)) * (z `2))] by GROUP_1:def 3
.= [((((x `1) * ((y `2) * (z `2))) + (((y `1) * (z `2)) * (x `2))) + (((z `1) * (y `2)) * (x `2))),(((x `2) * (y `2)) * (z `2))] by GROUP_1:def 3
.= [((((x `1) * ((y `2) * (z `2))) + (((y `1) * (z `2)) * (x `2))) + (((z `1) * (y `2)) * (x `2))),((x `2) * ((y `2) * (z `2)))] by GROUP_1:def 3
.= [(((x `1) * ((y `2) * (z `2))) + ((((y `1) * (z `2)) * (x `2)) + (((z `1) * (y `2)) * (x `2)))),((x `2) * ((y `2) * (z `2)))] by RLVECT_1:def 3
.= Fracadd (x,(Fracadd (y,z))) by VECTSP_1:def 7 ;
hence Fracadd (x,(Fracadd (y,z))) = Fracadd ((Fracadd (x,y)),z) ; :: thesis: verum