let T be RealLinearSpace; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum