let g1, g2 be Function of [:REAL ,(LinComb V):],(LinComb V); :: thesis: ( ( for a being Real
for e being Element of LinComb V holds g1 . [a,e] = a * (@ e) ) & ( for a being Real
for e being Element of LinComb V holds g2 . [a,e] = a * (@ e) ) implies g1 = g2 )
assume A3: for a being Real
for e being Element of LinComb V holds g1 . [a,e] = a * (@ e) ; :: thesis: ( ex a being Real ex e being Element of LinComb V st not g2 . [a,e] = a * (@ e) or g1 = g2 )
assume A4: for a being Real
for e being Element of LinComb V holds g2 . [a,e] = a * (@ e) ; :: thesis: g1 = g2

now

let x be Element of REAL ; :: thesis: for e being Element of LinComb V holds g1 . x,e = g2 . x,e
let e be Element of LinComb V; :: thesis: g1 . x,e = g2 . x,e
thus g1 . x,e = x * (@ e) by A3
.= g2 . x,e by A4 ; :: thesis: verum

end;

hence g1 = g2 by BINOP_1:2; :: thesis: verum