let A, B be real-membered set ; 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; ( y in B ++ A iff ex x, z being Real st
( x in B & z in A & y = x + z ) )
hereby ( 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
;
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;
ex w being Real st
( x in B & w in A & y = x + w )take w =
w;
( x in B & w in A & y = x + w )thus
(
x in B &
w in A &
y = x + w )
by A1;
verum
end;
given w, z being Real such that A2:
( w in B & z in A & y = w + z )
; y in B ++ A
thus
y in B ++ A
by A2; verum