defpred S₁[ Element of COMPLEX , Element of C_LinComb V, set ] means ex a being Complex st
( a = $1 & $3 = a * (@ $2) );
A1: for x being Element of COMPLEX
for e1 being Element of C_LinComb V ex e2 being Element of C_LinComb V st S₁[x,e1,e2]

proof

let x be Element of COMPLEX ; :: thesis: for e1 being Element of C_LinComb V ex e2 being Element of C_LinComb V st S₁[x,e1,e2]
let e1 be Element of C_LinComb V; :: thesis: ex e2 being Element of C_LinComb V st S₁[x,e1,e2]
take @ (x * (@ e1)) ; :: thesis: S₁[x,e1, @ (x * (@ e1))]
take x ; :: thesis: ( x = x & @ (x * (@ e1)) = x * (@ e1) )
thus ( x = x & @ (x * (@ e1)) = x * (@ e1) ) ; :: thesis: verum

end;

consider g being Function of [:COMPLEX,(C_LinComb V):],(C_LinComb V) such that
A2: for x being Element of COMPLEX
for e being Element of C_LinComb V holds S₁[x,e,g . (x,e)] from BINOP_1:sch 3(A1);
take g ; :: thesis: for a being Complex
for e being Element of C_LinComb V holds g . [a,e] = a * (@ e)
let a be Complex; :: thesis: for e being Element of C_LinComb V holds g . [a,e] = a * (@ e)
let e be Element of C_LinComb V; :: thesis: g . [a,e] = a * (@ e)
a in COMPLEX by XCMPLX_0:def 2;
then ex b being Complex st
( b = a & g . (a,e) = b * (@ e) ) by A2;
hence g . [a,e] = a * (@ e) ; :: thesis: verum