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 Real st
( x in B & w in A & y = x + w )
then consider x, w being Complex such that
A1: ( y = x + w & x in B & w in A ) ;
reconsider x = x, w = w as Real by A1;
take x = x; :: thesis: ex w being 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 A1; :: thesis: verum

end;

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