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

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)

hence
g1 = g2
; :: thesis: verumfor 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;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