defpred S1[ Real, Element of LinComb V, set ] means ex a being Real st
( a = \$1 & \$3 = a * (@ \$2) );
A1: for x being Element of REAL
for e1 being Element of LinComb V ex e2 being Element of LinComb V st S1[x,e1,e2]
proof
let x be Element of REAL ; :: thesis: for e1 being Element of LinComb V ex e2 being Element of LinComb V st S1[x,e1,e2]
let e1 be Element of LinComb V; :: thesis: ex e2 being Element of LinComb V st S1[x,e1,e2]
take @ (x * (@ e1)) ; :: thesis: S1[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 [:REAL,():],() such that
A2: for x being Element of REAL
for e being Element of LinComb V holds S1[x,e,g . (x,e)] from take g ; :: thesis: for a being Real
for e being Element of LinComb V holds g . [a,e] = a * (@ e)

let a be Real; :: thesis: for e being Element of LinComb V holds g . [a,e] = a * (@ e)
let e be Element of LinComb V; :: thesis: g . [a,e] = a * (@ e)
reconsider aa = a as Element of REAL by XREAL_0:def 1;
ex b being Real st
( b = aa & g . (aa,e) = b * (@ e) ) by A2;
hence g . [a,e] = a * (@ e) ; :: thesis: verum