let n be Nat; :: thesis: for r being Real
for q being Element of (TOP-REAL n)
for g being Element of (REAL-NS n) st q = g holds
r * q = r * g
let r be Real; :: thesis: for q being Element of (TOP-REAL n)
for g being Element of (REAL-NS n) st q = g holds
r * q = r * g
let q be Element of (TOP-REAL n); :: thesis: for g being Element of (REAL-NS n) st q = g holds
r * q = r * g
let g be Element of (REAL-NS n); :: thesis: ( q = g implies r * q = r * g )
assume A1: q = g ; :: thesis: r * q = r * g
thus r * q = the Mult of RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the addF of (TOP-REAL n), the Mult of (TOP-REAL n) #) . (r,q)
.= the Mult of RLSStruct(# the carrier of (REAL-NS n), the ZeroF of (REAL-NS n), the addF of (REAL-NS n), the Mult of (REAL-NS n) #) . (r,q) by Th1
.= r * g by A1 ; :: thesis: verum