assume that
A1: x = a and
A2: y = b ; :: thesis: x + y = a + b
reconsider a1 = a, b1 = b as Element of REAL n by A1, A2, REAL_NS1:def 6;
thus x + y = (Euclid_add n) . (a1,b1) by A1, A2, REAL_NS1:def 6
.= a + b by REAL_NS1:def 1 ; :: thesis: verum