let T be RealLinearSpace; for x, y being Element of T
for p, q being Tuple of 1, REAL st T = TOP-REAL 1 & p = x & q = y holds
x + y = p + q
let x, y be Element of T; for p, q being Tuple of 1, REAL st T = TOP-REAL 1 & p = x & q = y holds
x + y = p + q
let p, q be Tuple of 1, REAL ; ( T = TOP-REAL 1 & p = x & q = y implies x + y = p + q )
assume that
A1:
T = TOP-REAL 1
and
A2:
p = x
and
A3:
q = y
; x + y = p + q
A4:
( p in Funcs ((Seg 1),REAL) & q is Element of Funcs ((Seg 1),REAL) )
by SRINGS_5:11;
the addF of RLSStruct(# the carrier of (TOP-REAL 1), the ZeroF of (TOP-REAL 1), the addF of (TOP-REAL 1), the Mult of (TOP-REAL 1) #) . (p,q) =
the addF of (RealVectSpace (Seg 1)) . (p,q)
by EUCLID:def 8
.=
p + q
by A4, FUNCSDOM:def 1
;
hence
x + y = p + q
by A1, A2, A3, ALGSTR_0:def 1; verum