let G be non empty Abelian add-associative addLoopStr ; :: thesis: for x, y, z, t being Element of G holds (x + y) + (z + t) = (x + z) + (y + t)
let x, y, z, t be Element of G; :: thesis: (x + y) + (z + t) = (x + z) + (y + t)
thus (x + y) + (z + t) = x + (y + (z + t)) by RLVECT_1:def 3
.= x + (z + (y + t)) by RLVECT_1:def 3
.= (x + z) + (y + t) by RLVECT_1:def 3 ; :: thesis: verum