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 :: thesis: for x being Element of REAL
for e being Element of LinComb V holds g1 . (x,e) = g2 . (x,e)

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 ; :: thesis: verum