let X be Subset of REAL ; :: thesis: for q3, p3 being Real holds q3 ++ (p3 ++ X) = (q3 + p3) ++ X
let q3, p3 be Real; :: thesis: q3 ++ (p3 ++ X) = (q3 + p3) ++ X

now

let x be set ; :: thesis: ( ( x in q3 ++ (p3 ++ X) implies x in (q3 + p3) ++ X ) & ( x in (q3 + p3) ++ X implies x in q3 ++ (p3 ++ X) ) )

hereby :: thesis: ( x in (q3 + p3) ++ X implies x in q3 ++ (p3 ++ X) )

assume x in q3 ++ (p3 ++ X) ; :: thesis: x in (q3 + p3) ++ X
then consider r3 being Real such that
A1: x = q3 + r3 and
A2: r3 in p3 ++ X ;
consider q being Real such that
A3: r3 = p3 + q and
A4: q in X by A2;
x = (q3 + p3) + q by A1, A3;
hence x in (q3 + p3) ++ X by A4; :: thesis: verum

end;

assume x in (q3 + p3) ++ X ; :: thesis: x in q3 ++ (p3 ++ X)
then consider r3 being Real such that
A5: x = (q3 + p3) + r3 and
A6: r3 in X ;
p3 + r3 in p3 ++ X by A6;
then q3 + (p3 + r3) in q3 ++ (p3 ++ X) ;
hence x in q3 ++ (p3 ++ X) by A5; :: thesis: verum

end;

hence q3 ++ (p3 ++ X) = (q3 + p3) ++ X by TARSKI:2; :: thesis: verum