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

now

let x be Element of COMPLEX ; :: thesis: for e being Element of C_LinComb V holds g1 . x,e = g2 . x,e
let e be Element of C_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