let A, B be real-membered set ; :: thesis: for y being Real holds
( y in B ++ A iff ex x, z being Real st
( x in B & z in A & y = x + z ) )
let y be Real; :: thesis: ( y in B ++ A iff ex x, z being Real st
( x in B & z in A & y = x + z ) )

hereby :: thesis: ( ex x, z being Real st
( x in B & z in A & y = x + z ) implies y in B ++ A )

assume y in B ++ A ; :: thesis: ex x, w being Element of REAL st
( x in B & w in A & y = x + w )
then consider x, w being Element of COMPLEX such that
A2: ( y = x + w & x in B & w in A ) ;
( B c= REAL & A c= REAL ) by MEMBERED:3;
then reconsider x = x, w = w as Element of REAL by A2;
take x = x; :: thesis: ex w being Element of REAL st
( x in B & w in A & y = x + w )
take w = w; :: thesis: ( x in B & w in A & y = x + w )
thus ( x in B & w in A & y = x + w ) by A2; :: thesis: verum

end;

given w, z being Real such that A3: ( w in B & z in A & y = w + z ) ; :: thesis: y in B ++ A
thus y in B ++ A by A3, MEMBER_1:46; :: thesis: verum