let T be RealLinearSpace; :: thesis: for x, y being Element of T
for a being Real
for p, q being Tuple of 1, REAL st T = TOP-REAL 1 & p = x & q = y & x = a * y holds
p = a * q
let x, y be Element of T; :: thesis: for a being Real
for p, q being Tuple of 1, REAL st T = TOP-REAL 1 & p = x & q = y & x = a * y holds
p = a * q
let a be Real; :: thesis: for p, q being Tuple of 1, REAL st T = TOP-REAL 1 & p = x & q = y & x = a * y holds
p = a * q
let p, q be Tuple of 1, REAL ; :: thesis: ( T = TOP-REAL 1 & p = x & q = y & x = a * y implies p = a * q )
assume that
A1: T = TOP-REAL 1 and
A2: p = x and
A3: q = y and
A4: x = a * y ; :: thesis: p = a * q
set p9 = q;
A5: q in Funcs ((Seg 1),REAL) by SRINGS_5:11;
the Mult 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) #) . (a,q) = the Mult of (RealVectSpace (Seg 1)) . (a,q) by EUCLID:def 8
.= multreal [;] (a,q) by A5, FUNCSDOM:def 3
.= multreal .: (((dom q) --> a),q) by FUNCOP_1:31
.= a * q by Th22 ;
hence p = a * q by A1, A2, A3, A4; :: thesis: verum