let V be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for v, w being Element of V holds Sum <*v,w*> = (Sum <*v*>) + (Sum <*w*>)
let v, w be Element of V; :: thesis: Sum <*v,w*> = (Sum <*v*>) + (Sum <*w*>)
thus Sum <*v,w*> = v + w by Th45
.= (Sum <*v*>) + w by Lm6
.= (Sum <*v*>) + (Sum <*w*>) by Lm6 ; :: thesis: verum