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 (x + y) * z,(x * z) + (y * z) Fr_Eq S
let S be non empty multiplicatively-closed Subset of R; :: thesis: for x, y, z being Element of Frac S holds (x + y) * z,(x * z) + (y * z) Fr_Eq S
let x, y, z be Element of Frac S; :: thesis: (x + y) * z,(x * z) + (y * z) Fr_Eq S
A1: ((x `1) * (z `1)) * ((y `2) * (z `2)) = (((x `1) * (z `1)) * (y `2)) * (z `2) by GROUP_1:def 3
.= (((x `1) * (y `2)) * (z `1)) * (z `2) by GROUP_1:def 3
.= ((x `1) * (y `2)) * ((z `1) * (z `2)) by GROUP_1:def 3 ;
((y `1) * (z `1)) * ((x `2) * (z `2)) = (((y `1) * (z `1)) * (x `2)) * (z `2) by GROUP_1:def 3
.= (((y `1) * (x `2)) * (z `1)) * (z `2) by GROUP_1:def 3
.= ((y `1) * (x `2)) * ((z `1) * (z `2)) by GROUP_1:def 3 ;
then A3: Fracadd ((Fracmult (x,z)),(Fracmult (y,z))) = [((((x `1) * (y `2)) + ((y `1) * (x `2))) * ((z `1) * (z `2))),(((x `2) * (z `2)) * ((y `2) * (z `2)))] by A1, VECTSP_1:def 7;
((Fracmult ((Fracadd (x,y)),z)) `1) * ((Fracadd ((Fracmult (x,z)),(Fracmult (y,z)))) `2) = ((((x `1) * (y `2)) + ((y `1) * (x `2))) * (z `1)) * ((((z `2) * (x `2)) * (y `2)) * (z `2)) by GROUP_1:def 3
.= ((((x `1) * (y `2)) + ((y `1) * (x `2))) * (z `1)) * (((z `2) * ((x `2) * (y `2))) * (z `2)) by GROUP_1:def 3
.= (((((x `1) * (y `2)) + ((y `1) * (x `2))) * (z `1)) * (z `2)) * (((x `2) * (y `2)) * (z `2)) by GROUP_1:def 3
.= ((Fracadd ((Fracmult (x,z)),(Fracmult (y,z)))) `1) * ((Fracmult ((Fracadd (x,y)),z)) `2) by A3, GROUP_1:def 3 ;
then A5: ((((Fracmult ((Fracadd (x,y)),z)) `1) * ((Fracadd ((Fracmult (x,z)),(Fracmult (y,z)))) `2)) - (((Fracadd ((Fracmult (x,z)),(Fracmult (y,z)))) `1) * ((Fracmult ((Fracadd (x,y)),z)) `2))) * (1. R) = 0. R by RLVECT_1:5;
1. R is Element of S by C0SP1:def 4;
hence (x + y) * z,(x * z) + (y * z) Fr_Eq S by A5; :: thesis: verum