let T be RealLinearSpace; :: thesis: for x, y being Element of T
for a being Real
for p, q being Element of (TOP-REAL 1) 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 Element of (TOP-REAL 1) 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 Element of (TOP-REAL 1) st T = TOP-REAL 1 & p = x & q = y & x = a * y holds
p = a * q
let p, q be Element of (TOP-REAL 1); :: 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
( p is Element of REAL 1 & q is Element of REAL 1 ) by EUCLID:22;
then reconsider p9 = p, q9 = q as Tuple of 1, REAL ;
p9 = a * q9 by A1, A2, A3, A4, Th23;
hence p = a * q ; :: thesis: verum