for X being Subset of REAL
for q3, p3 being Real holds q3 ++ (p3 ++ X) = (q3 + p3) ++ X by MEMBER_1:147;