let g1, g2 be Function of [: the carrier of R,(LinComb V):],(LinComb V); :: thesis: ( ( for a being Element of R

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

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

assume A3: for a being Element of R

for e being Element of LinComb V holds g1 . [a,e] = a * (@ e) ; :: thesis: ( ex a being Element of R ex e being Element of LinComb V st not g2 . [a,e] = a * (@ e) or g1 = g2 )

assume A4: for a being Element of R

for e being Element of LinComb V holds g2 . [a,e] = a * (@ e) ; :: thesis: g1 = g2

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

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

assume A3: for a being Element of R

for e being Element of LinComb V holds g1 . [a,e] = a * (@ e) ; :: thesis: ( ex a being Element of R ex e being Element of LinComb V st not g2 . [a,e] = a * (@ e) or g1 = g2 )

assume A4: for a being Element of R

for e being Element of LinComb V holds g2 . [a,e] = a * (@ e) ; :: thesis: g1 = g2

now :: thesis: for x being Element of R

for e being Element of LinComb V holds g1 . (x,e) = g2 . (x,e)

hence
g1 = g2
; :: thesis: verumfor e being Element of LinComb V holds g1 . (x,e) = g2 . (x,e)

let x be Element of R; :: 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;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