defpred S_{1}[ Element of R, Element of LinComb V, set ] means ex a being Element of R st

( a = $1 & $3 = a * (@ $2) );

A1: for x being Element of R

for e1 being Element of LinComb V ex e2 being Element of LinComb V st S_{1}[x,e1,e2]

A2: for x being Element of R

for e being Element of LinComb V holds S_{1}[x,e,g . (x,e)]
from BINOP_1:sch 3(A1);

take g ; :: thesis: for a being Element of R

for e being Element of LinComb V holds g . [a,e] = a * (@ e)

let a be Element of R; :: 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 a0 = a as Element of R ;

ex b being Element of R st

( b = a0 & g . (a0,e) = b * (@ e) ) by A2;

hence g . [a,e] = a * (@ e) ; :: thesis: verum

( a = $1 & $3 = a * (@ $2) );

A1: for x being Element of R

for e1 being Element of LinComb V ex e2 being Element of LinComb V st S

proof

consider g being Function of [: the carrier of R,(LinComb V):],(LinComb V) such that
let x be Element of R; :: thesis: for e1 being Element of LinComb V ex e2 being Element of LinComb V st S_{1}[x,e1,e2]

let e1 be Element of LinComb V; :: thesis: ex e2 being Element of LinComb V st S_{1}[x,e1,e2]

take @ (x * (@ e1)) ; :: thesis: S_{1}[x,e1, @ (x * (@ e1))]

take x ; :: thesis: ( x = x & @ (x * (@ e1)) = x * (@ e1) )

thus ( x = x & @ (x * (@ e1)) = x * (@ e1) ) ; :: thesis: verum

end;let e1 be Element of LinComb V; :: thesis: ex e2 being Element of LinComb V st S

take @ (x * (@ e1)) ; :: thesis: S

take x ; :: thesis: ( x = x & @ (x * (@ e1)) = x * (@ e1) )

thus ( x = x & @ (x * (@ e1)) = x * (@ e1) ) ; :: thesis: verum

A2: for x being Element of R

for e being Element of LinComb V holds S

take g ; :: thesis: for a being Element of R

for e being Element of LinComb V holds g . [a,e] = a * (@ e)

let a be Element of R; :: 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 a0 = a as Element of R ;

ex b being Element of R st

( b = a0 & g . (a0,e) = b * (@ e) ) by A2;

hence g . [a,e] = a * (@ e) ; :: thesis: verum