let F be Ring; :: thesis: for E being RingExtension of F
for a, b being Element of E
for s being Element of F
for v being Element of (VecSp (E,F)) st a = s & b = v holds
a * b = s * v
let E be RingExtension of F; :: thesis: for a, b being Element of E
for s being Element of F
for v being Element of (VecSp (E,F)) st a = s & b = v holds
a * b = s * v
let a, b be Element of E; :: thesis: for s being Element of F
for v being Element of (VecSp (E,F)) st a = s & b = v holds
a * b = s * v
let s be Element of F; :: thesis: for v being Element of (VecSp (E,F)) st a = s & b = v holds
a * b = s * v
let v be Element of (VecSp (E,F)); :: 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,F)) = the carrier of E by FIELD_4:def 6;
then A2: [s,v] in [: the carrier of F, the carrier of E:] by ZFMISC_1:def 2;
thus s * v = ( the multF of E | [: the carrier of F, the carrier of E:]) . (s,v) by FIELD_4:def 6
.= a * b by A1, A2, FUNCT_1:49 ; :: thesis: verum