theorem
:: SUPINF_2:3
for
x
,
y
being
ExtReal
for
a
,
b
being
Real
st
x
=
a
&
y
=
b
holds
x

y
=
a

b