let R be Ring; :: thesis: for E being RingExtension of R
for a, b being Element of E
for s being Element of R
for v being Element of (VecSp (E,R)) st a = s & b = v holds
a * b = s * v
let E be RingExtension of R; :: thesis: for a, b being Element of E
for s being Element of R
for v being Element of (VecSp (E,R)) st a = s & b = v holds
a * b = s * v
let a, b be Element of E; :: thesis: for s being Element of R
for v being Element of (VecSp (E,R)) st a = s & b = v holds
a * b = s * v
let s be Element of R; :: thesis: for v being Element of (VecSp (E,R)) st a = s & b = v holds
a * b = s * v
let v be Element of (VecSp (E,R)); :: thesis: ( a = s & b = v implies a * b = s * v )
assume A1: ( a = s & b = v ) ; :: thesis: a * b = s * v
the carrier of (VecSp (E,R)) = the carrier of E by Def5;
then A2: [s,v] in [: the carrier of R, the carrier of E:] by ZFMISC_1:def 2;
thus s * v = ( the multF of E | [: the carrier of R, the carrier of E:]) . (s,v) by Def5
.= a * b by A1, A2, FUNCT_1:49 ; :: thesis: verum