let a, b be Functional of (RealVS V); :: thesis: ( ( for i being Element of V holds a . i = Re (l . i) ) & ( for i being Element of V holds b . i = Re (l . i) ) implies a = b )
assume A2: for i being Element of V holds a . i = Re (l . i) ; :: thesis: ( ex i being Element of V st not b . i = Re (l . i) or a = b )
assume A3: for i being Element of V holds b . i = Re (l . i) ; :: thesis: a = b

now :: thesis: for i being Element of (RealVS V) holds a . i = b . i

let i be Element of (RealVS V); :: thesis: a . i = b . i
addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
then reconsider j = i as Element of V ;
thus a . i = Re (l . j) by A2
.= b . i by A3 ; :: thesis: verum

end;

hence a = b by FUNCT_2:63; :: thesis: verum